normform.miz

    begin

    reserve A,B for non empty preBoolean set,

x,y for Element of [:A, B:];

    definition

      let A, B, x, y;

      :: NORMFORM:def1

      pred x c= y means (x `1 ) c= (y `1 ) & (x `2 ) c= (y `2 );

      reflexivity ;

      :: NORMFORM:def2

      func x \/ y -> Element of [:A, B:] equals [((x `1 ) \/ (y `1 )), ((x `2 ) \/ (y `2 ))];

      correctness ;

      commutativity ;

      idempotence by MCART_1: 21;

      :: NORMFORM:def3

      func x /\ y -> Element of [:A, B:] equals [((x `1 ) /\ (y `1 )), ((x `2 ) /\ (y `2 ))];

      correctness ;

      commutativity ;

      idempotence by MCART_1: 21;

      :: NORMFORM:def4

      func x \ y -> Element of [:A, B:] equals [((x `1 ) \ (y `1 )), ((x `2 ) \ (y `2 ))];

      correctness ;

      :: NORMFORM:def5

      func x \+\ y -> Element of [:A, B:] equals [((x `1 ) \+\ (y `1 )), ((x `2 ) \+\ (y `2 ))];

      correctness ;

      commutativity ;

    end

    reserve X for set,

a,b,c for Element of [:A, B:];

    theorem :: NORMFORM:1



     Th1: a c= b & b c= a implies a = b

    proof

      assume (a `1 ) c= (b `1 ) & (a `2 ) c= (b `2 ) & (b `1 ) c= (a `1 ) & (b `2 ) c= (a `2 );

      then (a `1 ) = (b `1 ) & (a `2 ) = (b `2 );

      hence thesis by DOMAIN_1: 2;

    end;

    theorem :: NORMFORM:2



     Th2: a c= b & b c= c implies a c= c

    proof

      assume (a `1 ) c= (b `1 ) & (a `2 ) c= (b `2 ) & (b `1 ) c= (c `1 ) & (b `2 ) c= (c `2 );

      hence (a `1 ) c= (c `1 ) & (a `2 ) c= (c `2 );

    end;

    theorem :: NORMFORM:3



     Th3: ((a \/ b) \/ c) = (a \/ (b \/ c))

    proof



       A1: (((a \/ b) \/ c) `2 ) = (((a \/ b) `2 ) \/ (c `2 ))

      .= (((a `2 ) \/ (b `2 )) \/ (c `2 ))

      .= ((a `2 ) \/ ((b `2 ) \/ (c `2 ))) by XBOOLE_1: 4

      .= ((a `2 ) \/ ((b \/ c) `2 ))

      .= ((a \/ (b \/ c)) `2 );

      (((a \/ b) \/ c) `1 ) = (((a \/ b) `1 ) \/ (c `1 ))

      .= (((a `1 ) \/ (b `1 )) \/ (c `1 ))

      .= ((a `1 ) \/ ((b `1 ) \/ (c `1 ))) by XBOOLE_1: 4

      .= ((a `1 ) \/ ((b \/ c) `1 ))

      .= ((a \/ (b \/ c)) `1 );

      hence thesis by A1, DOMAIN_1: 2;

    end;

    theorem :: NORMFORM:4

    ((a /\ b) /\ c) = (a /\ (b /\ c))

    proof



       A1: (((a /\ b) /\ c) `2 ) = (((a /\ b) `2 ) /\ (c `2 ))

      .= (((a `2 ) /\ (b `2 )) /\ (c `2 ))

      .= ((a `2 ) /\ ((b `2 ) /\ (c `2 ))) by XBOOLE_1: 16

      .= ((a `2 ) /\ ((b /\ c) `2 ))

      .= ((a /\ (b /\ c)) `2 );

      (((a /\ b) /\ c) `1 ) = (((a /\ b) `1 ) /\ (c `1 ))

      .= (((a `1 ) /\ (b `1 )) /\ (c `1 ))

      .= ((a `1 ) /\ ((b `1 ) /\ (c `1 ))) by XBOOLE_1: 16

      .= ((a `1 ) /\ ((b /\ c) `1 ))

      .= ((a /\ (b /\ c)) `1 );

      hence thesis by A1, DOMAIN_1: 2;

    end;

    theorem :: NORMFORM:5



     Th5: (a /\ (b \/ c)) = ((a /\ b) \/ (a /\ c))

    proof



       A1: ((a /\ (b \/ c)) `2 ) = ((a `2 ) /\ ((b \/ c) `2 ))

      .= ((a `2 ) /\ ((b `2 ) \/ (c `2 )))

      .= (((a `2 ) /\ (b `2 )) \/ ((a `2 ) /\ (c `2 ))) by XBOOLE_1: 23

      .= (((a `2 ) /\ (b `2 )) \/ ((a /\ c) `2 ))

      .= (((a /\ b) `2 ) \/ ((a /\ c) `2 ))

      .= (((a /\ b) \/ (a /\ c)) `2 );

      ((a /\ (b \/ c)) `1 ) = ((a `1 ) /\ ((b \/ c) `1 ))

      .= ((a `1 ) /\ ((b `1 ) \/ (c `1 )))

      .= (((a `1 ) /\ (b `1 )) \/ ((a `1 ) /\ (c `1 ))) by XBOOLE_1: 23

      .= (((a `1 ) /\ (b `1 )) \/ ((a /\ c) `1 ))

      .= (((a /\ b) `1 ) \/ ((a /\ c) `1 ))

      .= (((a /\ b) \/ (a /\ c)) `1 );

      hence thesis by A1, DOMAIN_1: 2;

    end;

    theorem :: NORMFORM:6



     Th6: (a \/ (b /\ a)) = a

    proof



       A1: ((a \/ (b /\ a)) `2 ) = ((a `2 ) \/ ((b /\ a) `2 ))

      .= ((a `2 ) \/ ((b `2 ) /\ (a `2 )))

      .= (a `2 ) by XBOOLE_1: 22;

      ((a \/ (b /\ a)) `1 ) = ((a `1 ) \/ ((b /\ a) `1 ))

      .= ((a `1 ) \/ ((b `1 ) /\ (a `1 )))

      .= (a `1 ) by XBOOLE_1: 22;

      hence thesis by A1, DOMAIN_1: 2;

    end;

    theorem :: NORMFORM:7



     Th7: (a /\ (b \/ a)) = a

    proof



      thus (a /\ (b \/ a)) = ((a /\ b) \/ (a /\ a)) by Th5

      .= a by Th6;

    end;

    theorem :: NORMFORM:8

    (a \/ (b /\ c)) = ((a \/ b) /\ (a \/ c))

    proof



      thus (a \/ (b /\ c)) = ((a \/ (c /\ a)) \/ (c /\ b)) by Th6

      .= (a \/ ((c /\ a) \/ (c /\ b))) by Th3

      .= (a \/ (c /\ (a \/ b))) by Th5

      .= (((a \/ b) /\ a) \/ ((a \/ b) /\ c)) by Th7

      .= ((a \/ b) /\ (a \/ c)) by Th5;

    end;

    theorem :: NORMFORM:9



     Th9: a c= c & b c= c implies (a \/ b) c= c by XBOOLE_1: 8;

    theorem :: NORMFORM:10



     Th10: a c= (a \/ b) & b c= (a \/ b) by XBOOLE_1: 7;

    theorem :: NORMFORM:11

    a = (a \/ b) implies b c= a by Th10;

    theorem :: NORMFORM:12



     Th12: a c= b implies (c \/ a) c= (c \/ b) & (a \/ c) c= (b \/ c) by XBOOLE_1: 9;

    theorem :: NORMFORM:13

    ((a \ b) \/ b) = (a \/ b)

    proof

      (((a `1 ) \ (b `1 )) \/ (b `1 )) = ((a `1 ) \/ (b `1 )) & (((a `2 ) \ (b `2 )) \/ (b `2 )) = ((a `2 ) \/ (b `2 )) by XBOOLE_1: 39;

      hence thesis;

    end;

    theorem :: NORMFORM:14

    (a \ b) c= c implies a c= (b \/ c) by XBOOLE_1: 44;

    theorem :: NORMFORM:15

    a c= (b \/ c) implies (a \ c) c= b by XBOOLE_1: 43;

    reserve a for Element of [:( Fin X), ( Fin X):];

    definition

      let A be set;

      :: NORMFORM:def6

      func FinPairUnion A -> BinOp of [:( Fin A), ( Fin A):] means

      : Def6: for x,y be Element of [:( Fin A), ( Fin A):] holds (it . (x,y)) = (x \/ y);

      existence

      proof

        deffunc O( Element of [:( Fin A), ( Fin A):], Element of [:( Fin A), ( Fin A):]) = ($1 \/ $2);

        ex IT be BinOp of [:( Fin A), ( Fin A):] st for x,y be Element of [:( Fin A), ( Fin A):] holds (IT . (x,y)) = O(x,y) from BINOP_1:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let IT,IT9 be BinOp of [:( Fin A), ( Fin A):] such that

         A1: for x,y be Element of [:( Fin A), ( Fin A):] holds (IT . (x,y)) = (x \/ y) and

         A2: for x,y be Element of [:( Fin A), ( Fin A):] holds (IT9 . (x,y)) = (x \/ y);

        now

          let x,y be Element of [:( Fin A), ( Fin A):];



          thus (IT . (x,y)) = (x \/ y) by A1

          .= (IT9 . (x,y)) by A2;

        end;

        hence IT = IT9;

      end;

    end

    reserve A for set;

    definition

      let X be non empty set, A be set;

      let B be Element of ( Fin X);

      let f be Function of X, [:( Fin A), ( Fin A):];

      :: NORMFORM:def7

      func FinPairUnion (B,f) -> Element of [:( Fin A), ( Fin A):] equals (( FinPairUnion A) $$ (B,f));

      correctness ;

    end



     Lm1: ( FinPairUnion A) is idempotent

    proof

      let a be Element of [:( Fin A), ( Fin A):];



      thus (( FinPairUnion A) . (a,a)) = (a \/ a) by Def6

      .= a;

    end;



     Lm2: ( FinPairUnion A) is commutative

    proof

      let a,b be Element of [:( Fin A), ( Fin A):];



      thus (( FinPairUnion A) . (a,b)) = (b \/ a) by Def6

      .= (( FinPairUnion A) . (b,a)) by Def6;

    end;



     Lm3: ( FinPairUnion A) is associative

    proof

      let a,b,c be Element of [:( Fin A), ( Fin A):];



      thus (( FinPairUnion A) . (a,(( FinPairUnion A) . (b,c)))) = (a \/ (( FinPairUnion A) . (b,c))) by Def6

      .= (a \/ (b \/ c)) by Def6

      .= ((a \/ b) \/ c) by Th3

      .= ((( FinPairUnion A) . (a,b)) \/ c) by Def6

      .= (( FinPairUnion A) . ((( FinPairUnion A) . (a,b)),c)) by Def6;

    end;

    registration

      let A be set;

      cluster ( FinPairUnion A) -> commutative idempotent associative;

      coherence by Lm1, Lm2, Lm3;

    end

    theorem :: NORMFORM:16

    for X be non empty set holds for f be Function of X, [:( Fin A), ( Fin A):] holds for B be Element of ( Fin X) holds for x be Element of X st x in B holds (f . x) c= ( FinPairUnion (B,f))

    proof

      let X be non empty set, f be Function of X, [:( Fin A), ( Fin A):];

      let B be Element of ( Fin X), x be Element of X;

      assume

       A1: x in B;



      then (( FinPairUnion A) $$ (B,f)) = (( FinPairUnion A) $$ ((B \/ {.x.}),f)) by ZFMISC_1: 40

      .= (( FinPairUnion A) . ((( FinPairUnion A) $$ (B,f)),(f . x))) by A1, SETWISEO: 20

      .= ((( FinPairUnion A) $$ (B,f)) \/ (f . x)) by Def6;

      hence thesis by Th10;

    end;

    theorem :: NORMFORM:17



     Th17: [( {}. A), ( {}. A)] is_a_unity_wrt ( FinPairUnion A)

    proof

      now

        let x be Element of [:( Fin A), ( Fin A):];



        thus (( FinPairUnion A) . ( [( {}. A), ( {}. A)],x)) = ( [( {}. A), ( {}. A)] \/ x) by Def6

        .= x by MCART_1: 21;

      end;

      hence thesis by BINOP_1: 4;

    end;

    theorem :: NORMFORM:18



     Th18: ( FinPairUnion A) is having_a_unity

    proof

       [( {}. A), ( {}. A)] is_a_unity_wrt ( FinPairUnion A) by Th17;

      hence thesis by SETWISEO:def 2;

    end;

    theorem :: NORMFORM:19



     Th19: ( the_unity_wrt ( FinPairUnion A)) = [( {}. A), ( {}. A)]

    proof

       [( {}. A), ( {}. A)] is_a_unity_wrt ( FinPairUnion A) by Th17;

      hence thesis by BINOP_1:def 8;

    end;

    theorem :: NORMFORM:20



     Th20: for x be Element of [:( Fin A), ( Fin A):] holds ( the_unity_wrt ( FinPairUnion A)) c= x

    proof

      let x be Element of [:( Fin A), ( Fin A):];

       [( {}. A), ( {}. A)] is_a_unity_wrt ( FinPairUnion A) by Th17;

      then ( the_unity_wrt ( FinPairUnion A)) = [ {} , {} ] by BINOP_1:def 8;

      then (( the_unity_wrt ( FinPairUnion A)) `1 ) = {} & (( the_unity_wrt ( FinPairUnion A)) `2 ) = {} ;

      hence (( the_unity_wrt ( FinPairUnion A)) `1 ) c= (x `1 ) & (( the_unity_wrt ( FinPairUnion A)) `2 ) c= (x `2 );

    end;

    theorem :: NORMFORM:21

    for X be non empty set holds for f be Function of X, [:( Fin A), ( Fin A):], B be Element of ( Fin X) holds for c be Element of [:( Fin A), ( Fin A):] st for x be Element of X st x in B holds (f . x) c= c holds ( FinPairUnion (B,f)) c= c

    proof

      let X be non empty set, f be Function of X, [:( Fin A), ( Fin A):];

      let B be Element of ( Fin X), c be Element of [:( Fin A), ( Fin A):];

      defpred P[ Element of ( Fin X)] means $1 c= B implies (( FinPairUnion A) $$ ($1,f)) c= c;

      assume

       A1: for x be Element of X st x in B holds (f . x) c= c;

       A2:

      now

        let C be Element of ( Fin X), b be Element of X;

        assume

         A3: P[C];

        now

          assume

           A4: (C \/ {b}) c= B;

          then {b} c= B by XBOOLE_1: 11;

          then b in B by ZFMISC_1: 31;

          then

           A5: (f . b) c= c by A1;

          (( FinPairUnion A) $$ ((C \/ {.b.}),f)) = (( FinPairUnion A) . ((( FinPairUnion A) $$ (C,f)),(f . b))) by Th18, SETWISEO: 32

          .= ((( FinPairUnion A) $$ (C,f)) \/ (f . b)) by Def6;

          hence (( FinPairUnion A) $$ ((C \/ {.b.}),f)) c= c by A3, A4, A5, Th9, XBOOLE_1: 11;

        end;

        hence P[(C \/ {.b.})];

      end;



       A6: P[( {}. X)]

      proof

        assume ( {}. X) c= B;

        (( FinPairUnion A) $$ (( {}. X),f)) = ( the_unity_wrt ( FinPairUnion A)) by Th18, SETWISEO: 31;

        hence thesis by Th20;

      end;

      for C be Element of ( Fin X) holds P[C] from SETWISEO:sch 4( A6, A2);

      hence thesis;

    end;

    theorem :: NORMFORM:22

    for X be non empty set, B be Element of ( Fin X) holds for f,g be Function of X, [:( Fin A), ( Fin A):] st (f | B) = (g | B) holds ( FinPairUnion (B,f)) = ( FinPairUnion (B,g))

    proof

      let X be non empty set, B be Element of ( Fin X);

      let f,g be Function of X, [:( Fin A), ( Fin A):];

      set J = ( FinPairUnion A);



       A1: [( {}. A), ( {}. A)] = ( the_unity_wrt J) by Th19;

      assume

       A2: (f | B) = (g | B);

      now

        per cases ;

          suppose

           A3: B = {} ;



          hence ( FinPairUnion (B,f)) = (J $$ (( {}. X),f))

          .= [( {}. A), ( {}. A)] by A1, Th18, SETWISEO: 31

          .= (J $$ (( {}. X),g)) by A1, Th18, SETWISEO: 31

          .= ( FinPairUnion (B,g)) by A3;

        end;

          suppose

           A4: B <> {} ;

          (f .: B) = (g .: B) by A2, RELAT_1: 166;

          hence thesis by A4, SETWISEO: 26;

        end;

      end;

      hence thesis;

    end;

    definition

      let X;

      :: NORMFORM:def8

      func DISJOINT_PAIRS (X) -> Subset of [:( Fin X), ( Fin X):] equals { a : (a `1 ) misses (a `2 ) };

      coherence

      proof

        set D = { a : (a `1 ) misses (a `2 ) };

        D c= [:( Fin X), ( Fin X):]

        proof

          let x be object;

          assume x in D;

          then ex a st x = a & (a `1 ) misses (a `2 );

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let X;

      cluster ( DISJOINT_PAIRS X) -> non empty;

      coherence

      proof

         {} is Element of ( Fin X) by FINSUB_1: 7;

        then

        reconsider b = [ {} , {} ] as Element of [:( Fin X), ( Fin X):] by ZFMISC_1:def 2;

        (b `1 ) misses (b `2 );

        then b in { a : (a `1 ) misses (a `2 ) };

        hence thesis;

      end;

    end

    theorem :: NORMFORM:23



     Th23: for y be Element of [:( Fin X), ( Fin X):] holds y in ( DISJOINT_PAIRS X) iff (y `1 ) misses (y `2 )

    proof

      let y be Element of [:( Fin X), ( Fin X):];

      y in ( DISJOINT_PAIRS X) iff ex a st y = a & (a `1 ) misses (a `2 );

      hence thesis;

    end;

    reserve x,y for Element of [:( Fin X), ( Fin X):],

a,b for Element of ( DISJOINT_PAIRS X);

    theorem :: NORMFORM:24

    y in ( DISJOINT_PAIRS X) & x in ( DISJOINT_PAIRS X) implies ((y \/ x) in ( DISJOINT_PAIRS X) iff (((y `1 ) /\ (x `2 )) \/ ((x `1 ) /\ (y `2 ))) = {} )

    proof

      assume that

       A1: y in ( DISJOINT_PAIRS X) and

       A2: x in ( DISJOINT_PAIRS X);



       A3: (((y `1 ) \/ (x `1 )) /\ ((y `2 ) \/ (x `2 ))) = ((((y `1 ) \/ (x `1 )) /\ (y `2 )) \/ (((y `1 ) \/ (x `1 )) /\ (x `2 ))) & (((y `1 ) \/ (x `1 )) /\ (y `2 )) = (((y `1 ) /\ (y `2 )) \/ ((x `1 ) /\ (y `2 ))) by XBOOLE_1: 23;

      (x `1 ) misses (x `2 ) by A2, Th23;

      then

       A4: ((x `1 ) /\ (x `2 )) = {} ;

      (y `1 ) misses (y `2 ) by A1, Th23;

      then

       A5: ((y `1 ) /\ (y `2 )) = {} ;



       A6: (((y `1 ) \/ (x `1 )) /\ (x `2 )) = (((y `1 ) /\ (x `2 )) \/ ((x `1 ) /\ (x `2 ))) by XBOOLE_1: 23;



       A7: ((y \/ x) `1 ) = ((y `1 ) \/ (x `1 )) & ((y \/ x) `2 ) = ((y `2 ) \/ (x `2 ));

      thus (y \/ x) in ( DISJOINT_PAIRS X) implies (((y `1 ) /\ (x `2 )) \/ ((x `1 ) /\ (y `2 ))) = {} by A5, A4, A7, A3, A6, XBOOLE_0:def 7, Th23;

      assume (((y `1 ) /\ (x `2 )) \/ ((x `1 ) /\ (y `2 ))) = {} ;

      then ((y \/ x) `1 ) misses ((y \/ x) `2 ) by A5, A4, A3, A6;

      hence thesis;

    end;

    theorem :: NORMFORM:25

    (a `1 ) misses (a `2 ) by Th23;

    theorem :: NORMFORM:26



     Th26: x c= b implies x is Element of ( DISJOINT_PAIRS X)

    proof

      assume

       A1: (x `1 ) c= (b `1 ) & (x `2 ) c= (b `2 );

      (b `1 ) misses (b `2 ) by Th23;

      then (x `1 ) misses (x `2 ) by A1, XBOOLE_1: 64;

      hence thesis by Th23;

    end;

    theorem :: NORMFORM:27



     Th27: not (ex x be set st x in (a `1 ) & x in (a `2 )) by Th23, XBOOLE_0: 3;

    theorem :: NORMFORM:28

     not (a \/ b) in ( DISJOINT_PAIRS X) implies ex p be Element of X st p in (a `1 ) & p in (b `2 ) or p in (b `1 ) & p in (a `2 )

    proof

      set p = the Element of (((a \/ b) `1 ) /\ ((a \/ b) `2 ));

      assume not (a \/ b) in ( DISJOINT_PAIRS X);

      then ((a \/ b) `1 ) meets ((a \/ b) `2 );

      then

       A1: (((a \/ b) `1 ) /\ ((a \/ b) `2 )) <> {} ;

      (((a \/ b) `1 ) /\ ((a \/ b) `2 )) is Subset of X by FINSUB_1: 16;

      then

      reconsider p as Element of X by A1, TARSKI:def 3;

      p in ((a \/ b) `2 ) by A1, XBOOLE_0:def 4;

      then p in ((a `2 ) \/ (b `2 ));

      then

       A2: p in (b `2 ) or p in (a `2 ) by XBOOLE_0:def 3;

      take p;

      p in ((a \/ b) `1 ) by A1, XBOOLE_0:def 4;

      then p in ((a `1 ) \/ (b `1 ));

      then p in (a `1 ) or p in (b `1 ) by XBOOLE_0:def 3;

      hence thesis by A2, Th27;

    end;

    theorem :: NORMFORM:29

    (x `1 ) misses (x `2 ) implies x is Element of ( DISJOINT_PAIRS X) by Th23;

    theorem :: NORMFORM:30

    for V,W be set st V c= (a `1 ) & W c= (a `2 ) holds [V, W] is Element of ( DISJOINT_PAIRS X)

    proof

      let V,W be set;

      assume

       A1: V c= (a `1 ) & W c= (a `2 );

      then V is Element of ( Fin X) & W is Element of ( Fin X) by SETWISEO: 11;

      then

      reconsider x = [V, W] as Element of [:( Fin X), ( Fin X):] by ZFMISC_1:def 2;

      (a `1 ) misses (a `2 ) & ( [V, W] `1 ) = V by Th23;

      then (x `1 ) misses (x `2 ) by A1, XBOOLE_1: 64;

      hence thesis by Th23;

    end;

    reserve A for set,

x for Element of [:( Fin A), ( Fin A):],

a,b,c,d,s,t for Element of ( DISJOINT_PAIRS A),

B,C,D for Element of ( Fin ( DISJOINT_PAIRS A));



     Lm4: for A holds {} in { B : a in B & b in B & a c= b implies a = b }

    proof

      let A;

       {} is Element of ( Fin ( DISJOINT_PAIRS A)) & for a, b holds a in {} & b in {} & a c= b implies a = b by FINSUB_1: 7;

      hence thesis;

    end;

    definition

      let A;

      :: NORMFORM:def9

      func Normal_forms_on A -> Subset of ( Fin ( DISJOINT_PAIRS A)) equals { B : a in B & b in B & a c= b implies a = b };

      coherence

      proof

        set IT = { B : a in B & b in B & a c= b implies a = b };

        IT c= ( Fin ( DISJOINT_PAIRS A))

        proof

          let x be object;

          assume x in IT;

          then ex B st x = B & for a, b holds a in B & b in B & a c= b implies a = b;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let A;

      cluster ( Normal_forms_on A) -> non empty;

      coherence by Lm4;

    end

    reserve K,L,M for Element of ( Normal_forms_on A);

    theorem :: NORMFORM:31

     {} in ( Normal_forms_on A) by Lm4;

    theorem :: NORMFORM:32



     Th32: B in ( Normal_forms_on A) & a in B & b in B & a c= b implies a = b

    proof

      assume B in ( Normal_forms_on A);

      then ex C st B = C & for a, b holds a in C & b in C & a c= b implies a = b;

      hence thesis;

    end;

    theorem :: NORMFORM:33



     Th33: (for a, b st a in B & b in B & a c= b holds a = b) implies B in ( Normal_forms_on A);

    definition

      let A, B;

      :: NORMFORM:def10

      func mi B -> Element of ( Normal_forms_on A) equals { t : s in B & s c= t iff s = t };

      coherence

      proof

        set M = { t : s in B & s c= t iff s = t };

        now

          let x be object;

          assume x in M;

          then ex t st x = t & for s holds s in B & s c= t iff s = t;

          hence x in B;

        end;

        then

         A1: M c= B;

        then

         A2: M is finite by FINSET_1: 1;

        B c= ( DISJOINT_PAIRS A) by FINSUB_1:def 5;

        then M c= ( DISJOINT_PAIRS A) by A1;

        then

        reconsider M9 = M as Element of ( Fin ( DISJOINT_PAIRS A)) by A2, FINSUB_1:def 5;

        now

          let c,d be Element of ( DISJOINT_PAIRS A);

          assume c in M;

          then ex t st c = t & for s holds s in B & s c= t iff s = t;

          then

           A3: c in B;

          assume d in M;

          then ex t st d = t & for s holds s in B & s c= t iff s = t;

          hence c c= d implies c = d by A3;

        end;

        then M9 is Element of ( Normal_forms_on A) by Th33;

        hence thesis;

      end;

      correctness ;

      let C;

      :: NORMFORM:def11

      func B ^ C -> Element of ( Fin ( DISJOINT_PAIRS A)) equals (( DISJOINT_PAIRS A) /\ { (s \/ t) : s in B & t in C });

      coherence

      proof

        deffunc F( Element of ( DISJOINT_PAIRS A), Element of ( DISJOINT_PAIRS A)) = ($1 \/ $2);

        set M = (( DISJOINT_PAIRS A) /\ { F(s,t) : s in B & t in C });



         A4: C is finite;



         A5: B is finite;

        { F(s,t) : s in B & t in C } is finite from FRAENKEL:sch 22( A5, A4);

        then M c= ( DISJOINT_PAIRS A) & M is finite by FINSET_1: 1, XBOOLE_1: 17;

        hence thesis by FINSUB_1:def 5;

      end;

      correctness ;

    end

    theorem :: NORMFORM:34



     Th34: x in (B ^ C) implies ex b, c st b in B & c in C & x = (b \/ c)

    proof

      assume x in (B ^ C);

      then x in { (s \/ t) : s in B & t in C } by XBOOLE_0:def 4;

      then ex s, t st x = (s \/ t) & s in B & t in C;

      hence thesis;

    end;

    theorem :: NORMFORM:35



     Th35: b in B & c in C & (b \/ c) in ( DISJOINT_PAIRS A) implies (b \/ c) in (B ^ C)

    proof

      assume b in B & c in C;

      then

       A1: (b \/ c) in { (s \/ t) : s in B & t in C };

      assume (b \/ c) in ( DISJOINT_PAIRS A);

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: NORMFORM:36



     Th36: a in ( mi B) implies a in B & (b in B & b c= a implies b = a)

    proof

      assume a in ( mi B);

      then ex t st a = t & for s holds s in B & s c= t iff s = t;

      hence thesis;

    end;

    theorem :: NORMFORM:37

    a in ( mi B) implies a in B by Th36;

    theorem :: NORMFORM:38

    a in ( mi B) & b in B & b c= a implies b = a by Th36;

    theorem :: NORMFORM:39



     Th39: a in B & (for b st b in B & b c= a holds b = a) implies a in ( mi B)

    proof

      assume a in B & for s st s in B & s c= a holds s = a;

      then s in B & s c= a iff s = a;

      hence thesis;

    end;



     Lm5: (for a holds a in B implies a in C) implies B c= C

    proof

      assume

       A1: for a holds a in B implies a in C;

      let x be object;

      assume

       A2: x in B;

      then x is Element of ( DISJOINT_PAIRS A) by SETWISEO: 9;

      hence thesis by A1, A2;

    end;

    theorem :: NORMFORM:40



     Th40: ( mi B) c= B

    proof

      for a holds a in ( mi B) implies a in B by Th36;

      hence thesis by Lm5;

    end;

    theorem :: NORMFORM:41



     Th41: b in B implies ex c st c c= b & c in ( mi B)

    proof

      assume

       A1: b in B;

      defpred P[ Element of ( DISJOINT_PAIRS A), Element of ( DISJOINT_PAIRS A)] means $1 c= $2;



       A2: for a holds P[a, a];



       A3: for a, b, c st P[a, b] & P[b, c] holds P[a, c] by Th2;

      for a st a in B holds ex b st b in B & P[b, a] & for c st c in B & P[c, b] holds P[b, c] from FRAENKEL:sch 23( A2, A3);

      then

      consider c such that

       A4: c in B and

       A5: c c= b and

       A6: for a st a in B & a c= c holds c c= a by A1;

      take c;

      thus c c= b by A5;

      now

        let b;

        assume that

         A7: b in B and

         A8: b c= c;

        c c= b by A6, A7, A8;

        hence b = c by A8, Th1;

      end;

      hence thesis by A4, Th39;

    end;

    theorem :: NORMFORM:42



     Th42: ( mi K) = K

    proof

      thus ( mi K) c= K by Th40;

      now

        let a;

        assume

         A1: a in K;

        then for b st b in K & b c= a holds b = a by Th32;

        hence a in ( mi K) by A1, Th39;

      end;

      hence thesis by Lm5;

    end;

    theorem :: NORMFORM:43



     Th43: ( mi (B \/ C)) c= (( mi B) \/ C)

    proof

      now

        let a;

        assume

         A1: a in ( mi (B \/ C));

        then

         A2: a in (B \/ C) by Th36;

        now

          per cases by A2, XBOOLE_0:def 3;

            suppose

             A3: a in B;

            now

              let b;

              assume b in B;

              then b in (B \/ C) by XBOOLE_0:def 3;

              hence b c= a implies b = a by A1, Th36;

            end;

            then a in ( mi B) by A3, Th39;

            hence a in (( mi B) \/ C) by XBOOLE_0:def 3;

          end;

            suppose a in C;

            hence a in (( mi B) \/ C) by XBOOLE_0:def 3;

          end;

        end;

        hence a in (( mi B) \/ C);

      end;

      hence thesis by Lm5;

    end;

    theorem :: NORMFORM:44



     Th44: ( mi (( mi B) \/ C)) = ( mi (B \/ C))

    proof



       A1: (( mi B) \/ C) c= (B \/ C) by Th40, XBOOLE_1: 9;

      now

        let a;

        assume

         A2: a in ( mi (( mi B) \/ C));

         A3:

        now

          let b;

          assume that

           A4: b in (B \/ C) and

           A5: b c= a;

          now

            per cases by A4, XBOOLE_0:def 3;

              suppose b in B;

              then

              consider c such that

               A6: c c= b and

               A7: c in ( mi B) by Th41;

              c in (( mi B) \/ C) & c c= a by A5, A6, A7, Th2, XBOOLE_0:def 3;

              then c = a by A2, Th36;

              hence b = a by A5, A6, Th1;

            end;

              suppose b in C;

              then b in (( mi B) \/ C) by XBOOLE_0:def 3;

              hence b = a by A2, A5, Th36;

            end;

          end;

          hence b = a;

        end;

        a in (( mi B) \/ C) by A2, Th36;

        hence a in ( mi (B \/ C)) by A1, A3, Th39;

      end;

      hence ( mi (( mi B) \/ C)) c= ( mi (B \/ C)) by Lm5;



       A8: ( mi (B \/ C)) c= (( mi B) \/ C) by Th43;

      now

        let a;

        assume

         A9: a in ( mi (B \/ C));

        then for b st b in (( mi B) \/ C) holds b c= a implies b = a by A1, Th36;

        hence a in ( mi (( mi B) \/ C)) by A8, A9, Th39;

      end;

      hence thesis by Lm5;

    end;

    theorem :: NORMFORM:45

    ( mi (B \/ ( mi C))) = ( mi (B \/ C)) by Th44;

    theorem :: NORMFORM:46



     Th46: B c= C implies (B ^ D) c= (C ^ D)

    proof

      deffunc F( Element of ( DISJOINT_PAIRS A), Element of ( DISJOINT_PAIRS A)) = ($1 \/ $2);

      defpred P[ set, set] means $1 in B & $2 in D;

      defpred Q[ set, set] means $1 in C & $2 in D;

      set X1 = { F(s,t) : P[s, t] };

      set X2 = { F(s,t) : Q[s, t] };

      assume B c= C;

      then

       A1: P[s, t] implies Q[s, t];

      X1 c= X2 from FRAENKEL:sch 2( A1);

      hence thesis by XBOOLE_1: 26;

    end;



     Lm6: a in (B ^ C) implies ex b st b c= a & b in (( mi B) ^ C)

    proof

      assume a in (B ^ C);

      then

      consider b, c such that

       A1: b in B and

       A2: c in C and

       A3: a = (b \/ c) by Th34;

      consider d such that

       A4: d c= b and

       A5: d in ( mi B) by A1, Th41;

      (d \/ c) c= a by A3, A4, Th12;

      then

      reconsider e = (d \/ c) as Element of ( DISJOINT_PAIRS A) by Th26;

      take e;

      thus e c= a by A3, A4, Th12;

      thus thesis by A2, A5, Th35;

    end;

    theorem :: NORMFORM:47



     Th47: ( mi (B ^ C)) c= (( mi B) ^ C)

    proof



       A1: (( mi B) ^ C) c= (B ^ C) by Th40, Th46;

      now

        let a;

        assume

         A2: a in ( mi (B ^ C));

        then a in (B ^ C) by Th36;

        then ex b st b c= a & b in (( mi B) ^ C) by Lm6;

        hence a in (( mi B) ^ C) by A1, A2, Th36;

      end;

      hence thesis by Lm5;

    end;

    theorem :: NORMFORM:48



     Th48: (B ^ C) = (C ^ B)

    proof

      deffunc F( Element of ( DISJOINT_PAIRS A), Element of ( DISJOINT_PAIRS A)) = ($1 \/ $2);

      defpred P[ set, set] means $1 in B & $2 in C;

      defpred Q[ set, set] means $2 in C & $1 in B;

      set X1 = { F(s,t) where s,t be Element of ( DISJOINT_PAIRS A) : P[s, t] };

      set X2 = { F(t,s) where s,t be Element of ( DISJOINT_PAIRS A) : Q[s, t] };



       A1: F(s,t) = F(t,s);

       A2:

      now

        let x be object;

        x in X2 iff ex s, t st x = (t \/ s) & t in C & s in B;

        then x in X2 iff ex t, s st x = (t \/ s) & t in C & s in B;

        hence x in X2 iff x in { (t \/ s) where t, s : t in C & s in B };

      end;



       A3: P[s, t] iff Q[s, t];

      X1 = X2 from FRAENKEL:sch 8( A3, A1);

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: NORMFORM:49



     Th49: B c= C implies (D ^ B) c= (D ^ C)

    proof

      (D ^ C) = (C ^ D) & (D ^ B) = (B ^ D) by Th48;

      hence thesis by Th46;

    end;

    theorem :: NORMFORM:50



     Th50: ( mi (( mi B) ^ C)) = ( mi (B ^ C))

    proof



       A1: (( mi B) ^ C) c= (B ^ C) by Th40, Th46;

      now

        let a;

        assume

         A2: a in ( mi (( mi B) ^ C));

         A3:

        now

          let b;

          assume b in (B ^ C);

          then

          consider c such that

           A4: c c= b and

           A5: c in (( mi B) ^ C) by Lm6;

          assume

           A6: b c= a;

          then c c= a by A4, Th2;

          then c = a by A2, A5, Th36;

          hence b = a by A4, A6, Th1;

        end;

        a in (( mi B) ^ C) by A2, Th36;

        hence a in ( mi (B ^ C)) by A1, A3, Th39;

      end;

      hence ( mi (( mi B) ^ C)) c= ( mi (B ^ C)) by Lm5;



       A7: ( mi (B ^ C)) c= (( mi B) ^ C) by Th47;

      now

        let a;

        assume

         A8: a in ( mi (B ^ C));

        then for b st b in (( mi B) ^ C) holds b c= a implies b = a by A1, Th36;

        hence a in ( mi (( mi B) ^ C)) by A7, A8, Th39;

      end;

      hence thesis by Lm5;

    end;

    theorem :: NORMFORM:51



     Th51: ( mi (B ^ ( mi C))) = ( mi (B ^ C))

    proof

      (B ^ ( mi C)) = (( mi C) ^ B) & (B ^ C) = (C ^ B) by Th48;

      hence thesis by Th50;

    end;

    theorem :: NORMFORM:52



     Th52: (K ^ (L ^ M)) = ((K ^ L) ^ M)

    proof



       A1: (L ^ M) = (M ^ L) & (K ^ L) = (L ^ K) by Th48;

       A2:

      now

        let K, L, M;

        now

          let a;

          assume a in (K ^ (L ^ M));

          then

          consider b, c such that

           A3: b in K and

           A4: c in (L ^ M) and

           A5: a = (b \/ c) by Th34;

          consider b1,c1 be Element of ( DISJOINT_PAIRS A) such that

           A6: b1 in L and

           A7: c1 in M and

           A8: c = (b1 \/ c1) by A4, Th34;

          reconsider d = (b \/ (b1 \/ c1)) as Element of ( DISJOINT_PAIRS A) by A5, A8;



           A9: (b \/ (b1 \/ c1)) = ((b \/ b1) \/ c1) by Th3;

          then (b \/ b1) c= d by Th10;

          then

          reconsider c2 = (b \/ b1) as Element of ( DISJOINT_PAIRS A) by Th26;

          c2 in (K ^ L) by A3, A6, Th35;

          hence a in ((K ^ L) ^ M) by A5, A7, A8, A9, Th35;

        end;

        hence (K ^ (L ^ M)) c= ((K ^ L) ^ M) by Lm5;

      end;

      then

       A10: (K ^ (L ^ M)) c= ((K ^ L) ^ M);

      ((K ^ L) ^ M) = (M ^ (K ^ L)) & (K ^ (L ^ M)) = ((L ^ M) ^ K) by Th48;

      then ((K ^ L) ^ M) c= (K ^ (L ^ M)) by A1, A2;

      hence thesis by A10;

    end;

    theorem :: NORMFORM:53



     Th53: (K ^ (L \/ M)) = ((K ^ L) \/ (K ^ M))

    proof

      now

        let a;

        assume a in (K ^ (L \/ M));

        then

        consider b, c such that

         A1: b in K and

         A2: c in (L \/ M) and

         A3: a = (b \/ c) by Th34;

        c in L or c in M by A2, XBOOLE_0:def 3;

        then a in (K ^ L) or a in (K ^ M) by A1, A3, Th35;

        hence a in ((K ^ L) \/ (K ^ M)) by XBOOLE_0:def 3;

      end;

      hence (K ^ (L \/ M)) c= ((K ^ L) \/ (K ^ M)) by Lm5;

      (K ^ L) c= (K ^ (L \/ M)) & (K ^ M) c= (K ^ (L \/ M)) by Th49, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;



     Lm7: a in (B ^ C) implies ex c st c in C & c c= a

    proof

      assume a in (B ^ C);

      then

      consider b, c such that b in B and

       A1: c in C and

       A2: a = (b \/ c) by Th34;

      take c;

      thus c in C by A1;

      thus thesis by A2, Th10;

    end;



     Lm8: ( mi ((K ^ L) \/ L)) = ( mi L)

    proof

      now

        let a;

        assume

         A1: a in ( mi ((K ^ L) \/ L));

         A2:

        now

          let b;

          assume b in L;

          then b in ((K ^ L) \/ L) by XBOOLE_0:def 3;

          hence b c= a implies b = a by A1, Th36;

        end;

         A3:

        now

          assume a in (K ^ L);

          then

          consider b such that

           A4: b in L and

           A5: b c= a by Lm7;

          b in ((K ^ L) \/ L) by A4, XBOOLE_0:def 3;

          hence a in L by A1, A4, A5, Th36;

        end;

        a in ((K ^ L) \/ L) by A1, Th36;

        then a in (K ^ L) or a in L by XBOOLE_0:def 3;

        hence a in ( mi L) by A3, A2, Th39;

      end;

      hence ( mi ((K ^ L) \/ L)) c= ( mi L) by Lm5;

      now

        let a;

        assume

         A6: a in ( mi L);

        then

         A7: a in L by Th36;

         A8:

        now

          let b;

          assume b in ((K ^ L) \/ L);

          then

           A9: b in (K ^ L) or b in L by XBOOLE_0:def 3;

          assume

           A10: b c= a;

          now

            assume b in (K ^ L);

            then

            consider c such that

             A11: c in L and

             A12: c c= b by Lm7;

            c c= a by A10, A12, Th2;

            then c = a by A6, A11, Th36;

            hence b in L by A7, A10, A12, Th1;

          end;

          hence b = a by A6, A9, A10, Th36;

        end;

        a in ((K ^ L) \/ L) by A7, XBOOLE_0:def 3;

        hence a in ( mi ((K ^ L) \/ L)) by A8, Th39;

      end;

      hence thesis by Lm5;

    end;

    theorem :: NORMFORM:54



     Th54: B c= (B ^ B)

    proof

      now

        let a;

        a = (a \/ a);

        hence a in B implies a in (B ^ B) by Th35;

      end;

      hence thesis by Lm5;

    end;

    theorem :: NORMFORM:55



     Th55: ( mi (K ^ K)) = ( mi K)

    proof



      thus ( mi (K ^ K)) = ( mi ((K ^ K) \/ K)) by Th54, XBOOLE_1: 12

      .= ( mi K) by Lm8;

    end;

    definition

      let A;

      :: NORMFORM:def12

      func NormForm A -> strict LattStr means

      : Def12: the carrier of it = ( Normal_forms_on A) & for B,C be Element of ( Normal_forms_on A) holds (the L_join of it . (B,C)) = ( mi (B \/ C)) & (the L_meet of it . (B,C)) = ( mi (B ^ C));

      existence

      proof

        set L = ( Normal_forms_on A);

        deffunc O( Element of L, Element of L) = ( mi ($1 \/ $2));

        consider j be BinOp of L such that

         A1: for x,y be Element of L holds (j . (x,y)) = O(x,y) from BINOP_1:sch 4;

        deffunc O1( Element of L, Element of L) = ( mi ($1 ^ $2));

        consider m be BinOp of L such that

         A2: for x,y be Element of L holds (m . (x,y)) = O1(x,y) from BINOP_1:sch 4;

        take LattStr (# L, j, m #);

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        set L = ( Normal_forms_on A);

        let A1,A2 be strict LattStr such that

         A3: the carrier of A1 = L and

         A4: for A,B be Element of L holds (the L_join of A1 . (A,B)) = ( mi (A \/ B)) & (the L_meet of A1 . (A,B)) = ( mi (A ^ B)) and

         A5: the carrier of A2 = L and

         A6: for A,B be Element of L holds (the L_join of A2 . (A,B)) = ( mi (A \/ B)) & (the L_meet of A2 . (A,B)) = ( mi (A ^ B));

        reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of L by A3, A5;

        now

          let x,y be Element of L;



          thus (a1 . (x,y)) = ( mi (x \/ y)) by A4

          .= (a2 . (x,y)) by A6;

        end;

        then

         A7: a1 = a2;

        now

          let x,y be Element of L;



          thus (a3 . (x,y)) = ( mi (x ^ y)) by A4

          .= (a4 . (x,y)) by A6;

        end;

        hence thesis by A3, A5, A7, BINOP_1: 2;

      end;

    end

    registration

      let A;

      cluster ( NormForm A) -> non empty;

      coherence

      proof

        the carrier of ( NormForm A) = ( Normal_forms_on A) by Def12;

        hence thesis;

      end;

    end



     Lm9: for a,b be Element of ( NormForm A) holds (a "\/" b) = (b "\/" a)

    proof

      set G = ( NormForm A);

      let a,b be Element of G;

      reconsider a9 = a, b9 = b as Element of ( Normal_forms_on A) by Def12;

      (a "\/" b) = ( mi (b9 \/ a9)) by Def12

      .= (b "\/" a) by Def12;

      hence thesis;

    end;



     Lm10: for a,b,c be Element of ( NormForm A) holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

    proof

      set G = ( NormForm A);

      let a,b,c be Element of G;

      reconsider a9 = a, b9 = b, c9 = c as Element of ( Normal_forms_on A) by Def12;

      (a "\/" (b "\/" c)) = (the L_join of G . (a,( mi (b9 \/ c9)))) by Def12

      .= ( mi (( mi (b9 \/ c9)) \/ a9)) by Def12

      .= ( mi (a9 \/ (b9 \/ c9))) by Th44

      .= ( mi ((a9 \/ b9) \/ c9)) by XBOOLE_1: 4

      .= ( mi (( mi (a9 \/ b9)) \/ c9)) by Th44

      .= (the L_join of G . (( mi (a9 \/ b9)),c9)) by Def12

      .= ((a "\/" b) "\/" c) by Def12;

      hence thesis;

    end;

    reserve K,L,M for Element of ( Normal_forms_on A);



     Lm11: (the L_join of ( NormForm A) . ((the L_meet of ( NormForm A) . (K,L)),L)) = L

    proof



      thus (the L_join of ( NormForm A) . ((the L_meet of ( NormForm A) . (K,L)),L)) = (the L_join of ( NormForm A) . (( mi (K ^ L)),L)) by Def12

      .= ( mi (( mi (K ^ L)) \/ L)) by Def12

      .= ( mi ((K ^ L) \/ L)) by Th44

      .= ( mi L) by Lm8

      .= L by Th42;

    end;



     Lm12: for a,b be Element of ( NormForm A) holds ((a "/\" b) "\/" b) = b

    proof

      let a,b be Element of ( NormForm A);

      reconsider a9 = a, b9 = b as Element of ( Normal_forms_on A) by Def12;

      set G = ( NormForm A);



      thus ((a "/\" b) "\/" b) = (the L_join of G . ((the L_meet of G . (a9,b9)),b9))

      .= b by Lm11;

    end;



     Lm13: for a,b be Element of ( NormForm A) holds (a "/\" b) = (b "/\" a)

    proof

      set G = ( NormForm A);

      let a,b be Element of G;

      reconsider a9 = a, b9 = b as Element of ( Normal_forms_on A) by Def12;

      (a "/\" b) = ( mi (a9 ^ b9)) by Def12

      .= ( mi (b9 ^ a9)) by Th48

      .= (b "/\" a) by Def12;

      hence thesis;

    end;



     Lm14: for a,b,c be Element of ( NormForm A) holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

    proof

      set G = ( NormForm A);

      let a,b,c be Element of G;

      reconsider a9 = a, b9 = b, c9 = c as Element of ( Normal_forms_on A) by Def12;

      (a "/\" (b "/\" c)) = (the L_meet of G . (a,( mi (b9 ^ c9)))) by Def12

      .= ( mi (a9 ^ ( mi (b9 ^ c9)))) by Def12

      .= ( mi (a9 ^ (b9 ^ c9))) by Th51

      .= ( mi ((a9 ^ b9) ^ c9)) by Th52

      .= ( mi (( mi (a9 ^ b9)) ^ c9)) by Th50

      .= (the L_meet of G . (( mi (a9 ^ b9)),c9)) by Def12

      .= ((a "/\" b) "/\" c) by Def12;

      hence thesis;

    end;



     Lm15: (the L_meet of ( NormForm A) . (K,(the L_join of ( NormForm A) . (L,M)))) = (the L_join of ( NormForm A) . ((the L_meet of ( NormForm A) . (K,L)),(the L_meet of ( NormForm A) . (K,M))))

    proof



       A1: (the L_meet of ( NormForm A) . (K,M)) = ( mi (K ^ M)) by Def12;

      (the L_join of ( NormForm A) . (L,M)) = ( mi (L \/ M)) & (the L_meet of ( NormForm A) . (K,L)) = ( mi (K ^ L)) by Def12;

      then

      reconsider La = (the L_join of ( NormForm A) . (L,M)), Lb = (the L_meet of ( NormForm A) . (K,L)), Lc = (the L_meet of ( NormForm A) . (K,M)) as Element of ( Normal_forms_on A) by A1;

      (the L_meet of ( NormForm A) . (K,(the L_join of ( NormForm A) . (L,M)))) = ( mi (K ^ La)) by Def12

      .= ( mi (K ^ ( mi (L \/ M)))) by Def12

      .= ( mi (K ^ (L \/ M))) by Th51

      .= ( mi ((K ^ L) \/ (K ^ M))) by Th53

      .= ( mi (( mi (K ^ L)) \/ (K ^ M))) by Th44

      .= ( mi (( mi (K ^ L)) \/ ( mi (K ^ M)))) by Th44

      .= ( mi (Lb \/ ( mi (K ^ M)))) by Def12

      .= ( mi (Lb \/ Lc)) by Def12;

      hence thesis by Def12;

    end;



     Lm16: for a,b be Element of ( NormForm A) holds (a "/\" (a "\/" b)) = a

    proof

      set G = ( NormForm A);

      let a,b be Element of G;

      reconsider a9 = a, b9 = b as Element of ( Normal_forms_on A) by Def12;



      thus (a "/\" (a "\/" b)) = (the L_join of G . ((the L_meet of G . (a9,a9)),(the L_meet of G . (a9,b9)))) by Lm15

      .= (the L_join of G . (( mi (a9 ^ a9)),(the L_meet of G . (a9,b9)))) by Def12

      .= (the L_join of G . (( mi a9),(the L_meet of G . (a9,b9)))) by Th55

      .= (a "\/" (a "/\" b)) by Th42

      .= ((a "/\" b) "\/" a) by Lm9

      .= ((b "/\" a) "\/" a) by Lm13

      .= a by Lm12;

    end;

    registration

      let A;

      cluster ( NormForm A) -> Lattice-like;

      coherence

      proof

        set G = ( NormForm A);

        thus for u,v be Element of G holds (u "\/" v) = (v "\/" u) by Lm9;

        thus for u,v,w be Element of G holds (u "\/" (v "\/" w)) = ((u "\/" v) "\/" w) by Lm10;

        thus for u,v be Element of G holds ((u "/\" v) "\/" v) = v by Lm12;

        thus for u,v be Element of G holds (u "/\" v) = (v "/\" u) by Lm13;

        thus for u,v,w be Element of G holds (u "/\" (v "/\" w)) = ((u "/\" v) "/\" w) by Lm14;

        let u,v be Element of G;

        thus thesis by Lm16;

      end;

    end

    registration

      let A;

      cluster ( NormForm A) -> distributive lower-bounded;

      coherence

      proof

        set G = ( NormForm A);

        thus G is distributive

        proof

          let u,v,w be Element of G;

          reconsider K = u, L = v, M = w as Element of ( Normal_forms_on A) by Def12;



          thus (u "/\" (v "\/" w)) = (the L_meet of G . (K,(the L_join of G . (L,M))))

          .= ((u "/\" v) "\/" (u "/\" w)) by Lm15;

        end;

        thus G is lower-bounded

        proof

          reconsider E = {} as Element of ( Normal_forms_on A) by Lm4;

          reconsider e = E as Element of G by Def12;

          take e;

          let u be Element of G;

          reconsider K = u as Element of ( Normal_forms_on A) by Def12;



           A1: (e "\/" u) = ( mi (E \/ K)) by Def12

          .= u by Th42;

          then (u "/\" e) = e by LATTICES:def 9;

          hence thesis by A1, LATTICES:def 9;

        end;

      end;

    end

    theorem :: NORMFORM:56

     {} is Element of ( NormForm A)

    proof

      the carrier of ( NormForm A) = ( Normal_forms_on A) by Def12;

      hence thesis by Lm4;

    end;

    theorem :: NORMFORM:57

    ( Bottom ( NormForm A)) = {}

    proof

       {} in ( Normal_forms_on A) by Lm4;

      then

      reconsider Z = {} as Element of ( NormForm A) by Def12;

      now

        let u be Element of ( NormForm A);

        reconsider z = Z, u9 = u as Element of ( Normal_forms_on A) by Def12;



        thus (Z "\/" u) = ( mi (z \/ u9)) by Def12

        .= u by Th42;

      end;

      hence thesis by LATTICE2: 14;

    end;