yellow_5.miz

    begin

    theorem :: YELLOW_5:1

    for L be reflexive antisymmetric with_suprema RelStr holds for a be Element of L holds (a "\/" a) = a

    proof

      let L be reflexive antisymmetric with_suprema RelStr, a be Element of L;

      a <= a;

      then a <= (a "\/" a) & (a "\/" a) <= a by YELLOW_0: 22;

      hence thesis by YELLOW_0:def 3;

    end;

    theorem :: YELLOW_5:2



     Th2: for L be reflexive antisymmetric with_infima RelStr holds for a be Element of L holds (a "/\" a) = a

    proof

      let L be reflexive antisymmetric with_infima RelStr, a be Element of L;

      a <= a;

      then (a "/\" a) <= a & a <= (a "/\" a) by YELLOW_0: 23;

      hence thesis by YELLOW_0:def 3;

    end;

    theorem :: YELLOW_5:3

    for L be transitive antisymmetric with_suprema RelStr holds for a,b,c be Element of L holds (a "\/" b) <= c implies a <= c

    proof

      let L be transitive antisymmetric with_suprema RelStr;

      let a,b,c be Element of L;



       A1: a <= (a "\/" b) by YELLOW_0: 22;

      assume (a "\/" b) <= c;

      hence thesis by A1, YELLOW_0:def 2;

    end;

    theorem :: YELLOW_5:4

    for L be transitive antisymmetric with_infima RelStr holds for a,b,c be Element of L holds c <= (a "/\" b) implies c <= a

    proof

      let L be transitive antisymmetric with_infima RelStr;

      let a,b,c be Element of L;



       A1: (a "/\" b) <= a by YELLOW_0: 23;

      assume c <= (a "/\" b);

      hence thesis by A1, YELLOW_0:def 2;

    end;

    theorem :: YELLOW_5:5

    for L be antisymmetric transitive with_suprema with_infima RelStr holds for a,b,c be Element of L holds (a "/\" b) <= (a "\/" c)

    proof

      let L be antisymmetric transitive with_suprema with_infima RelStr;

      let a,b,c be Element of L;

      (a "/\" b) <= a & a <= (a "\/" c) by YELLOW_0: 22, YELLOW_0: 23;

      hence thesis by YELLOW_0:def 2;

    end;

    theorem :: YELLOW_5:6



     Th6: for L be antisymmetric transitive with_infima RelStr holds for a,b,c be Element of L holds a <= b implies (a "/\" c) <= (b "/\" c)

    proof

      let L be antisymmetric transitive with_infima RelStr;

      let a,b,c be Element of L;



       A1: (a "/\" c) <= a by YELLOW_0: 23;



       A2: (a "/\" c) <= c by YELLOW_0: 23;

      assume a <= b;

      then (a "/\" c) <= b by A1, YELLOW_0:def 2;

      hence thesis by A2, YELLOW_0: 23;

    end;

    theorem :: YELLOW_5:7



     Th7: for L be antisymmetric transitive with_suprema RelStr holds for a,b,c be Element of L holds a <= b implies (a "\/" c) <= (b "\/" c)

    proof

      let L be non empty antisymmetric transitive with_suprema RelStr;

      let a,b,c be Element of L;



       A1: b <= (b "\/" c) by YELLOW_0: 22;



       A2: c <= (b "\/" c) by YELLOW_0: 22;

      assume a <= b;

      then a <= (b "\/" c) by A1, YELLOW_0:def 2;

      hence thesis by A2, YELLOW_0: 22;

    end;

    theorem :: YELLOW_5:8



     Th8: for L be sup-Semilattice holds for a,b be Element of L holds a <= b implies (a "\/" b) = b

    proof

      let L be sup-Semilattice;

      let a,b be Element of L;



       A1: b <= b;

      assume a <= b;

      then b <= (a "\/" b) & (a "\/" b) <= b by A1, YELLOW_0: 22;

      hence thesis by YELLOW_0:def 3;

    end;

    theorem :: YELLOW_5:9



     Th9: for L be sup-Semilattice holds for a,b,c be Element of L holds a <= c & b <= c implies (a "\/" b) <= c

    proof

      let L be sup-Semilattice;

      let a,b,c be Element of L;

      assume that

       A1: a <= c and

       A2: b <= c;

      (c "\/" b) = c by A2, Th8;

      hence thesis by A1, Th7;

    end;

    theorem :: YELLOW_5:10



     Th10: for L be Semilattice holds for a,b be Element of L holds b <= a implies (a "/\" b) = b

    proof

      let L be Semilattice;

      let a,b be Element of L;

      assume b <= a;

      then (b "/\" b) <= (a "/\" b) by Th6;

      then (a "/\" b) <= b & b <= (a "/\" b) by Th2, YELLOW_0: 23;

      hence thesis by YELLOW_0:def 3;

    end;

    begin

    theorem :: YELLOW_5:11



     Th11: for L be Boolean LATTICE, x,y be Element of L holds y is_a_complement_of x iff y = ( 'not' x)

    proof

      let L be Boolean LATTICE, x,y be Element of L;



       A1: for x be Element of L holds ( 'not' ( 'not' x)) = x by WAYBEL_1: 87;

      then

       A2: ( 'not' x) is_a_complement_of x by WAYBEL_1: 86;

      then

       A3: (x "/\" ( 'not' x)) = ( Bottom L) by WAYBEL_1:def 23;



       A4: (x "\/" ( 'not' x)) = ( Top L) by A2, WAYBEL_1:def 23;

      hereby

        assume

         A5: y is_a_complement_of x;

        then

         A6: (x "/\" y) = ( Bottom L) by WAYBEL_1:def 23;



         A7: ( Top L) >= ( 'not' x) by YELLOW_0: 45;



         A8: ( Bottom L) <= (y "/\" ( 'not' x)) by YELLOW_0: 44;

        ( Top L) >= y by YELLOW_0: 45;



        then

         A9: y = ((x "\/" ( 'not' x)) "/\" y) by A4, YELLOW_0: 25

        .= ((x "/\" y) "\/" (y "/\" ( 'not' x))) by WAYBEL_1:def 3

        .= (y "/\" ( 'not' x)) by A6, A8, YELLOW_0: 24;

        (x "\/" y) = ( Top L) by A5, WAYBEL_1:def 23;



        then ( 'not' x) = ((x "\/" y) "/\" ( 'not' x)) by A7, YELLOW_0: 25

        .= ((x "/\" ( 'not' x)) "\/" (y "/\" ( 'not' x))) by WAYBEL_1:def 3

        .= (y "/\" ( 'not' x)) by A3, A8, YELLOW_0: 24;

        hence y = ( 'not' x) by A9;

      end;

      thus thesis by A1, WAYBEL_1: 86;

    end;

    definition

      let L be non empty RelStr, a,b be Element of L;

      :: YELLOW_5:def1

      func a \ b -> Element of L equals (a "/\" ( 'not' b));

      correctness ;

    end

    definition

      let L be non empty RelStr, a,b be Element of L;

      :: YELLOW_5:def2

      func a \+\ b -> Element of L equals ((a \ b) "\/" (b \ a));

      correctness ;

    end

    definition

      let L be antisymmetric with_infima with_suprema RelStr, a,b be Element of L;

      :: original: \+\

      redefine

      func a \+\ b;

      commutativity

      proof

        let a,b be Element of L;



        thus (a \+\ b) = ((a \ b) "\/" (b \ a))

        .= (b \+\ a);

      end;

    end

    definition

      let L be non empty RelStr, a,b be Element of L;

      :: YELLOW_5:def3

      pred a meets b means (a "/\" b) <> ( Bottom L);

    end

    notation

      let L be non empty RelStr, a,b be Element of L;

      antonym a misses b for a meets b;

    end

    notation

      let L be with_infima antisymmetric RelStr, a,b be Element of L;

      antonym a misses b for a meets b;

    end

    definition

      let L be with_infima antisymmetric RelStr, a,b be Element of L;

      :: original: meets

      redefine

      pred a meets b;

      symmetry

      proof

        let a,b be Element of L;

        (a "/\" b) <> ( Bottom L) implies (b "/\" a) <> ( Bottom L);

        hence thesis;

      end;

    end

    theorem :: YELLOW_5:12

    for L be antisymmetric transitive with_infima with_suprema RelStr holds for a,b,c be Element of L holds a <= c implies (a \ b) <= c

    proof

      let L be antisymmetric transitive with_infima with_suprema RelStr;

      let a,b,c be Element of L;



       A1: (a "/\" ( 'not' b)) <= a by YELLOW_0: 23;

      assume a <= c;

      hence thesis by A1, YELLOW_0:def 2;

    end;

    theorem :: YELLOW_5:13

    for L be antisymmetric transitive with_infima with_suprema RelStr holds for a,b,c be Element of L holds a <= b implies (a \ c) <= (b \ c) by Th6;

    theorem :: YELLOW_5:14

    for L be LATTICE holds for a,b,c be Element of L holds (a \ b) <= c & (b \ a) <= c implies (a \+\ b) <= c by Th9;

    theorem :: YELLOW_5:15

    for L be LATTICE holds for a be Element of L holds a meets a iff a <> ( Bottom L) by Th2;

    theorem :: YELLOW_5:16

    for L be antisymmetric transitive with_infima RelStr st L is distributive holds for a,b,c be Element of L holds ((a "/\" b) "\/" (a "/\" c)) = a implies a <= (b "\/" c)

    proof

      let L be antisymmetric transitive with_infima RelStr such that

       A1: L is distributive;

      let a,b,c be Element of L;

      assume ((a "/\" b) "\/" (a "/\" c)) = a;

      then ((b "\/" c) "/\" a) = a by A1, WAYBEL_1:def 3;

      hence thesis by YELLOW_0: 23;

    end;

    theorem :: YELLOW_5:17



     Th17: for L be LATTICE st L is distributive holds for a,b,c be Element of L holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" (a "\/" c))

    proof

      let L be LATTICE such that

       A1: L is distributive;

      let a,b,c be Element of L;

      ((a "\/" b) "/\" (a "\/" c)) = (((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" c)) by A1, WAYBEL_1:def 3

      .= (a "\/" ((a "\/" b) "/\" c)) by LATTICE3: 18

      .= (a "\/" ((c "/\" a) "\/" (c "/\" b))) by A1, WAYBEL_1:def 3

      .= ((a "\/" (c "/\" a)) "\/" (c "/\" b)) by LATTICE3: 14

      .= (a "\/" (c "/\" b)) by LATTICE3: 17;

      hence thesis;

    end;

    theorem :: YELLOW_5:18

    for L be LATTICE st L is distributive holds for a,b,c be Element of L holds ((a "\/" b) \ c) = ((a \ c) "\/" (b \ c))

    proof

      let L be with_suprema with_infima reflexive transitive antisymmetric non empty RelStr such that

       A1: L is distributive;

      let a,b,c be Element of L;



      thus ((a "\/" b) \ c) = ((a "\/" b) "/\" ( 'not' c))

      .= ((( 'not' c) "/\" a) "\/" (( 'not' c) "/\" b)) by A1, WAYBEL_1:def 3

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

    end;

    begin

    theorem :: YELLOW_5:19



     Th19: for L be lower-bounded non empty antisymmetric RelStr holds for a be Element of L holds a <= ( Bottom L) implies a = ( Bottom L)

    proof

      let L be lower-bounded non empty antisymmetric RelStr;

      let a be Element of L;



       A1: ( Bottom L) <= a by YELLOW_0: 44;

      assume a <= ( Bottom L);

      hence thesis by A1, YELLOW_0:def 3;

    end;

    theorem :: YELLOW_5:20

    for L be lower-bounded Semilattice holds for a,b,c be Element of L holds a <= b & a <= c & (b "/\" c) = ( Bottom L) implies a = ( Bottom L)

    proof

      let L be lower-bounded Semilattice;

      let a,b,c be Element of L;

      assume that

       A1: a <= b and

       A2: a <= c and

       A3: (b "/\" c) = ( Bottom L);

      (a "/\" c) <= (b "/\" c) by A1, Th6;

      then a <= (b "/\" c) by A2, Th10;

      hence thesis by A3, Th19;

    end;

    theorem :: YELLOW_5:21

    for L be lower-bounded antisymmetric with_suprema RelStr holds for a,b be Element of L holds (a "\/" b) = ( Bottom L) implies a = ( Bottom L) & b = ( Bottom L)

    proof

      let L be lower-bounded antisymmetric with_suprema RelStr;

      let a,b be Element of L;

      assume (a "\/" b) = ( Bottom L);

      then a <= ( Bottom L) & b <= ( Bottom L) by YELLOW_0: 22;

      hence thesis by Th19;

    end;

    theorem :: YELLOW_5:22

    for L be lower-bounded antisymmetric transitive with_infima RelStr holds for a,b,c be Element of L holds a <= b & (b "/\" c) = ( Bottom L) implies (a "/\" c) = ( Bottom L)

    proof

      let L be lower-bounded antisymmetric transitive with_infima RelStr;

      let a,b,c be Element of L;

      assume a <= b & (b "/\" c) = ( Bottom L);

      then

       A1: (a "/\" c) <= ( Bottom L) by Th6;

      ( Bottom L) <= (a "/\" c) by YELLOW_0: 44;

      hence thesis by A1, YELLOW_0:def 3;

    end;

    theorem :: YELLOW_5:23

    for L be lower-bounded Semilattice holds for a be Element of L holds (( Bottom L) \ a) = ( Bottom L)

    proof

      let L be lower-bounded Semilattice;

      let a be Element of L;



      thus (( Bottom L) \ a) = (( Bottom L) "/\" ( 'not' a))

      .= ( Bottom L) by Th10, YELLOW_0: 44;

    end;

    theorem :: YELLOW_5:24

    for L be lower-bounded antisymmetric transitive with_infima RelStr holds for a,b,c be Element of L holds a meets b & b <= c implies a meets c

    proof

      let L be lower-bounded antisymmetric transitive with_infima RelStr;

      let a,b,c be Element of L;

      assume

       A1: a meets b;



       A2: ( Bottom L) <= (a "/\" b) by YELLOW_0: 44;

      assume b <= c;

      then

       A3: (a "/\" b) <= (a "/\" c) by Th6;

      assume not a meets c;

      then not (a "/\" c) <> ( Bottom L);

      then (a "/\" b) = ( Bottom L) by A3, A2, YELLOW_0:def 3;

      hence contradiction by A1;

    end;

    theorem :: YELLOW_5:25



     Th25: for L be lower-bounded with_infima antisymmetric RelStr holds for a be Element of L holds (a "/\" ( Bottom L)) = ( Bottom L)

    proof

      let L be lower-bounded with_infima antisymmetric RelStr;

      let a be Element of L;

      ( Bottom L) <= (a "/\" ( Bottom L)) & (a "/\" ( Bottom L)) <= ( Bottom L) by YELLOW_0: 23, YELLOW_0: 44;

      hence thesis by YELLOW_0:def 3;

    end;

    theorem :: YELLOW_5:26

    for L be lower-bounded antisymmetric transitive with_infima with_suprema RelStr holds for a,b,c be Element of L holds a meets (b "/\" c) implies a meets b

    proof

      let L be lower-bounded antisymmetric transitive with_infima with_suprema RelStr;

      let a,b,c be Element of L;

      assume

       A1: a meets (b "/\" c);

      assume

       A2: not a meets b;

      (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c) by LATTICE3: 16

      .= (( Bottom L) "/\" c) by A2

      .= ( Bottom L) by Th25;

      hence contradiction by A1;

    end;

    theorem :: YELLOW_5:27

    for L be lower-bounded antisymmetric transitive with_infima with_suprema RelStr holds for a,b,c be Element of L holds a meets (b \ c) implies a meets b

    proof

      let L be lower-bounded antisymmetric transitive with_infima with_suprema RelStr;

      let a,b,c be Element of L;

      assume

       A1: a meets (b \ c);

      assume

       A2: not a meets b;

      (a "/\" (b \ c)) = ((a "/\" b) "/\" ( 'not' c)) by LATTICE3: 16

      .= (( Bottom L) "/\" ( 'not' c)) by A2

      .= ( Bottom L) by Th25;

      hence contradiction by A1;

    end;

    theorem :: YELLOW_5:28

    for L be lower-bounded antisymmetric transitive with_infima RelStr holds for a be Element of L holds a misses ( Bottom L) by Th25;

    theorem :: YELLOW_5:29

    for L be lower-bounded antisymmetric transitive with_infima RelStr holds for a,b,c be Element of L holds a misses c & b <= c implies a misses b

    proof

      let L be lower-bounded antisymmetric transitive with_infima RelStr;

      let a,b,c be Element of L;

      assume that

       A1: a misses c and

       A2: b <= c;

      (a "/\" c) = ( Bottom L) by A1;

      then

       A3: (a "/\" b) <= ( Bottom L) by A2, Th6;

      ( Bottom L) <= (a "/\" b) by YELLOW_0: 44;

      then (a "/\" b) = ( Bottom L) by A3, YELLOW_0:def 3;

      hence thesis;

    end;

    theorem :: YELLOW_5:30

    for L be lower-bounded antisymmetric transitive with_infima RelStr holds for a,b,c be Element of L holds a misses b or a misses c implies a misses (b "/\" c)

    proof

      let L be lower-bounded antisymmetric transitive with_infima RelStr;

      let a,b,c be Element of L;

      assume

       A1: a misses b or a misses c;

      per cases by A1;

        suppose

         A2: a misses b;

        (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c) by LATTICE3: 16

        .= (( Bottom L) "/\" c) by A2

        .= ( Bottom L) by Th25;

        hence thesis;

      end;

        suppose

         A3: a misses c;

        (a "/\" (b "/\" c)) = ((a "/\" c) "/\" b) by LATTICE3: 16

        .= (( Bottom L) "/\" b) by A3

        .= ( Bottom L) by Th25;

        hence thesis;

      end;

    end;

    theorem :: YELLOW_5:31

    for L be lower-bounded LATTICE holds for a,b,c be Element of L holds a <= b & a <= c & b misses c implies a = ( Bottom L)

    proof

      let L be lower-bounded LATTICE;

      let a,b,c be Element of L;

      assume that

       A1: a <= b and

       A2: a <= c and

       A3: b misses c;

      (b "/\" c) = ( Bottom L) by A3;

      then ( Bottom L) <= (a "/\" c) & (a "/\" c) <= ( Bottom L) by A1, Th6, YELLOW_0: 44;

      then (a "/\" c) = ( Bottom L) by YELLOW_0:def 3;

      hence thesis by A2, Th10;

    end;

    theorem :: YELLOW_5:32

    for L be lower-bounded antisymmetric transitive with_infima RelStr holds for a,b,c be Element of L holds a misses b implies (a "/\" c) misses (b "/\" c)

    proof

      let L be lower-bounded antisymmetric transitive with_infima RelStr;

      let a,b,c be Element of L;

      assume

       A1: a misses b;

      ((a "/\" c) "/\" (b "/\" c)) = (c "/\" (a "/\" (b "/\" c))) by LATTICE3: 16

      .= ((c "/\" (a "/\" b)) "/\" c) by LATTICE3: 16

      .= ((c "/\" ( Bottom L)) "/\" c) by A1

      .= (( Bottom L) "/\" c) by Th25

      .= ( Bottom L) by Th25;

      hence thesis;

    end;

    begin

    reserve L for Boolean non empty RelStr;

    reserve a,b,c,d for Element of L;

    theorem :: YELLOW_5:33

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

    proof

      (((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a)) = (((a "\/" (b "/\" c)) "/\" (b "\/" (b "/\" c))) "\/" (c "/\" a)) by WAYBEL_1: 5

      .= (((a "\/" (b "/\" c)) "/\" b) "\/" (c "/\" a)) by LATTICE3: 17

      .= (((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" (b "\/" (c "/\" a))) by WAYBEL_1: 5

      .= (((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" ((b "\/" c) "/\" (b "\/" a))) by WAYBEL_1: 5

      .= (((b "/\" c) "\/" (a "\/" (c "/\" a))) "/\" ((b "\/" c) "/\" (b "\/" a))) by LATTICE3: 14

      .= (((b "/\" c) "\/" a) "/\" ((b "\/" c) "/\" (b "\/" a))) by LATTICE3: 17

      .= (((b "\/" a) "/\" (c "\/" a)) "/\" ((b "\/" c) "/\" (b "\/" a))) by WAYBEL_1: 5

      .= ((b "\/" a) "/\" (((c "\/" a) "/\" (b "\/" a)) "/\" (b "\/" c))) by LATTICE3: 16

      .= ((b "\/" a) "/\" ((b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c)))) by LATTICE3: 16

      .= (((b "\/" a) "/\" (b "\/" a)) "/\" ((c "\/" a) "/\" (b "\/" c))) by LATTICE3: 16

      .= ((b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c))) by Th2

      .= (((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)) by LATTICE3: 16;

      hence thesis;

    end;

    theorem :: YELLOW_5:34



     Th34: (a "/\" ( 'not' a)) = ( Bottom L) & (a "\/" ( 'not' a)) = ( Top L)

    proof

      ( 'not' a) is_a_complement_of a by Th11;

      hence thesis by WAYBEL_1:def 23;

    end;

    theorem :: YELLOW_5:35

    (a \ b) <= c implies a <= (b "\/" c)

    proof



       A1: a <= (a "\/" b) by YELLOW_0: 22;

      assume (a \ b) <= c;

      then

       A2: ((a "/\" ( 'not' b)) "\/" b) <= (c "\/" b) by Th7;

      ((a "/\" ( 'not' b)) "\/" b) = ((b "\/" a) "/\" (b "\/" ( 'not' b))) by Th17

      .= ((b "\/" a) "/\" ( Top L)) by Th34

      .= (a "\/" b) by WAYBEL_1: 4;

      hence thesis by A2, A1, YELLOW_0:def 2;

    end;

    theorem :: YELLOW_5:36



     Th36: ( 'not' (a "\/" b)) = (( 'not' a) "/\" ( 'not' b)) & ( 'not' (a "/\" b)) = (( 'not' a) "\/" ( 'not' b))

    proof



       A1: ((a "\/" b) "/\" (( 'not' a) "/\" ( 'not' b))) = (((a "\/" b) "/\" ( 'not' a)) "/\" ( 'not' b)) by LATTICE3: 16

      .= (((( 'not' a) "/\" a) "\/" (( 'not' a) "/\" b)) "/\" ( 'not' b)) by WAYBEL_1:def 3

      .= ((( Bottom L) "\/" (( 'not' a) "/\" b)) "/\" ( 'not' b)) by Th34

      .= ((( 'not' a) "/\" b) "/\" ( 'not' b)) by WAYBEL_1: 3

      .= (( 'not' a) "/\" (b "/\" ( 'not' b))) by LATTICE3: 16

      .= (( 'not' a) "/\" ( Bottom L)) by Th34

      .= ( Bottom L) by WAYBEL_1: 3;

      ((a "\/" b) "\/" (( 'not' a) "/\" ( 'not' b))) = (a "\/" (b "\/" (( 'not' a) "/\" ( 'not' b)))) by LATTICE3: 14

      .= (a "\/" ((b "\/" ( 'not' a)) "/\" (b "\/" ( 'not' b)))) by Th17

      .= (a "\/" ((b "\/" ( 'not' a)) "/\" ( Top L))) by Th34

      .= (a "\/" (b "\/" ( 'not' a))) by WAYBEL_1: 4

      .= ((a "\/" ( 'not' a)) "\/" b) by LATTICE3: 14

      .= (( Top L) "\/" b) by Th34

      .= ( Top L) by WAYBEL_1: 4;

      then (( 'not' a) "/\" ( 'not' b)) is_a_complement_of (a "\/" b) by A1, WAYBEL_1:def 23;

      hence ( 'not' (a "\/" b)) = (( 'not' a) "/\" ( 'not' b)) by Th11;



       A2: ((a "/\" b) "/\" (( 'not' a) "\/" ( 'not' b))) = (a "/\" (b "/\" (( 'not' a) "\/" ( 'not' b)))) by LATTICE3: 16

      .= (a "/\" ((b "/\" ( 'not' a)) "\/" (b "/\" ( 'not' b)))) by WAYBEL_1:def 3

      .= (a "/\" ((b "/\" ( 'not' a)) "\/" ( Bottom L))) by Th34

      .= (a "/\" (b "/\" ( 'not' a))) by WAYBEL_1: 3

      .= ((a "/\" ( 'not' a)) "/\" b) by LATTICE3: 16

      .= (( Bottom L) "/\" b) by Th34

      .= ( Bottom L) by WAYBEL_1: 3;

      ((a "/\" b) "\/" (( 'not' a) "\/" ( 'not' b))) = (((a "/\" b) "\/" ( 'not' a)) "\/" ( 'not' b)) by LATTICE3: 14

      .= (((( 'not' a) "\/" a) "/\" (( 'not' a) "\/" b)) "\/" ( 'not' b)) by Th17

      .= ((( Top L) "/\" (( 'not' a) "\/" b)) "\/" ( 'not' b)) by Th34

      .= ((( 'not' a) "\/" b) "\/" ( 'not' b)) by WAYBEL_1: 4

      .= (( 'not' a) "\/" (b "\/" ( 'not' b))) by LATTICE3: 14

      .= (( 'not' a) "\/" ( Top L)) by Th34

      .= ( Top L) by WAYBEL_1: 4;

      then (( 'not' a) "\/" ( 'not' b)) is_a_complement_of (a "/\" b) by A2, WAYBEL_1:def 23;

      hence ( 'not' (a "/\" b)) = (( 'not' a) "\/" ( 'not' b)) by Th11;

    end;

    theorem :: YELLOW_5:37



     Th37: a <= b implies ( 'not' b) <= ( 'not' a)

    proof

      assume a <= b;



      then ( 'not' a) = ( 'not' (b "/\" a)) by Th10

      .= (( 'not' b) "\/" ( 'not' a)) by Th36;

      hence thesis by YELLOW_0: 22;

    end;

    theorem :: YELLOW_5:38

    a <= b implies (c \ b) <= (c \ a)

    proof

      assume a <= b;

      then ( 'not' b) <= ( 'not' a) by Th37;

      then (c "/\" ( 'not' b)) <= (c "/\" ( 'not' a)) by Th6;

      hence thesis;

    end;

    theorem :: YELLOW_5:39

    a <= b & c <= d implies (a \ d) <= (b \ c)

    proof

      assume that

       A1: a <= b and

       A2: c <= d;

      ( 'not' d) <= ( 'not' c) by A2, Th37;

      then

       A3: (a "/\" ( 'not' d)) <= (a "/\" ( 'not' c)) by Th6;

      (a "/\" ( 'not' c)) <= (b "/\" ( 'not' c)) by A1, Th6;

      hence thesis by A3, YELLOW_0:def 2;

    end;

    theorem :: YELLOW_5:40

    a <= (b "\/" c) implies (a \ b) <= c & (a \ c) <= b

    proof

      assume

       A1: a <= (b "\/" c);

      ((b "\/" c) "/\" ( 'not' b)) = ((( 'not' b) "/\" b) "\/" (( 'not' b) "/\" c)) by WAYBEL_1:def 3

      .= (( Bottom L) "\/" (( 'not' b) "/\" c)) by Th34

      .= (c "/\" ( 'not' b)) by WAYBEL_1: 3;

      then (c "/\" ( 'not' b)) <= c & (a "/\" ( 'not' b)) <= (c "/\" ( 'not' b)) by A1, Th6, YELLOW_0: 23;

      hence (a \ b) <= c by YELLOW_0:def 2;

      ((b "\/" c) "/\" ( 'not' c)) = ((( 'not' c) "/\" b) "\/" (( 'not' c) "/\" c)) by WAYBEL_1:def 3

      .= ((( 'not' c) "/\" b) "\/" ( Bottom L)) by Th34

      .= (( 'not' c) "/\" b) by WAYBEL_1: 3;

      then (( 'not' c) "/\" b) <= b & (a "/\" ( 'not' c)) <= (( 'not' c) "/\" b) by A1, Th6, YELLOW_0: 23;

      hence thesis by YELLOW_0:def 2;

    end;

    theorem :: YELLOW_5:41

    ( 'not' a) <= ( 'not' (a "/\" b)) & ( 'not' b) <= ( 'not' (a "/\" b))

    proof

      ( 'not' a) <= (( 'not' a) "\/" ( 'not' b)) & ( 'not' b) <= (( 'not' a) "\/" ( 'not' b)) by YELLOW_0: 22;

      hence thesis by Th36;

    end;

    theorem :: YELLOW_5:42

    ( 'not' (a "\/" b)) <= ( 'not' a) & ( 'not' (a "\/" b)) <= ( 'not' b)

    proof

      (( 'not' a) "/\" ( 'not' b)) <= ( 'not' a) & (( 'not' a) "/\" ( 'not' b)) <= ( 'not' b) by YELLOW_0: 23;

      hence thesis by Th36;

    end;

    theorem :: YELLOW_5:43

    a <= (b \ a) implies a = ( Bottom L)

    proof

      assume

       A1: a <= (b \ a);

      ((b "/\" ( 'not' a)) "/\" a) = (b "/\" (( 'not' a) "/\" a)) by LATTICE3: 16

      .= (b "/\" ( Bottom L)) by Th34

      .= ( Bottom L) by WAYBEL_1: 3;

      hence thesis by A1, Th10;

    end;

    theorem :: YELLOW_5:44

    a <= b implies b = (a "\/" (b \ a))

    proof

      assume

       A1: a <= b;

      (a "\/" (b \ a)) = ((a "\/" b) "/\" (a "\/" ( 'not' a))) by WAYBEL_1: 5

      .= (b "/\" (( 'not' a) "\/" a)) by A1, Th8

      .= (b "/\" ( Top L)) by Th34

      .= b by WAYBEL_1: 4;

      hence thesis;

    end;

    theorem :: YELLOW_5:45

    (a \ b) = ( Bottom L) iff a <= b

    proof

      thus (a \ b) = ( Bottom L) implies a <= b

      proof

        assume (a \ b) = ( Bottom L);

        then ((b "\/" a) "/\" (b "\/" ( 'not' b))) <= (b "\/" ( Bottom L)) by Th17;

        then ((b "\/" a) "/\" (b "\/" ( 'not' b))) <= b by WAYBEL_1: 3;

        then ((a "\/" b) "/\" ( Top L)) <= b by Th34;

        then

         A1: (a "\/" b) <= b by WAYBEL_1: 4;

        a <= (a "\/" b) by YELLOW_0: 22;

        hence thesis by A1, YELLOW_0:def 2;

      end;

      thus a <= b implies (a \ b) = ( Bottom L)

      proof

        assume a <= b;

        then (a "/\" ( 'not' b)) <= (b "/\" ( 'not' b)) by Th6;

        then

         A2: (a "/\" ( 'not' b)) <= ( Bottom L) by Th34;

        ( Bottom L) <= (a \ b) by YELLOW_0: 44;

        hence thesis by A2, YELLOW_0:def 3;

      end;

    end;

    theorem :: YELLOW_5:46

    a <= (b "\/" c) & (a "/\" c) = ( Bottom L) implies a <= b

    proof

      assume a <= (b "\/" c) & (a "/\" c) = ( Bottom L);

      then (a "/\" (b "\/" c)) = a & (a "/\" (b "\/" c)) = ((a "/\" b) "\/" ( Bottom L)) by Th10, WAYBEL_1:def 3;

      then (a "/\" b) = a by WAYBEL_1: 3;

      hence thesis by YELLOW_0: 23;

    end;

    theorem :: YELLOW_5:47

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

    proof



      thus ((a \ b) "\/" b) = ((b "\/" a) "/\" (b "\/" ( 'not' b))) by Th17

      .= ((b "\/" a) "/\" ( Top L)) by Th34

      .= (a "\/" b) by WAYBEL_1: 4;

    end;

    theorem :: YELLOW_5:48

    (a \ (a "\/" b)) = ( Bottom L)

    proof



      thus (a \ (a "\/" b)) = (a "/\" (( 'not' a) "/\" ( 'not' b))) by Th36

      .= ((a "/\" ( 'not' a)) "/\" ( 'not' b)) by LATTICE3: 16

      .= (( Bottom L) "/\" ( 'not' b)) by Th34

      .= ( Bottom L) by WAYBEL_1: 3;

    end;

    theorem :: YELLOW_5:49

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

    proof



      thus (a \ (a "/\" b)) = (a "/\" (( 'not' a) "\/" ( 'not' b))) by Th36

      .= ((a "/\" ( 'not' a)) "\/" (a "/\" ( 'not' b))) by WAYBEL_1:def 3

      .= (( Bottom L) "\/" (a "/\" ( 'not' b))) by Th34

      .= (a \ b) by WAYBEL_1: 3;

    end;

    theorem :: YELLOW_5:50

    ((a \ b) "/\" b) = ( Bottom L)

    proof



      thus ((a \ b) "/\" b) = (a "/\" (( 'not' b) "/\" b)) by LATTICE3: 16

      .= (a "/\" ( Bottom L)) by Th34

      .= ( Bottom L) by WAYBEL_1: 3;

    end;

    theorem :: YELLOW_5:51

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

    proof



      thus (a "\/" (b \ a)) = ((a "\/" b) "/\" (a "\/" ( 'not' a))) by Th17

      .= ((a "\/" b) "/\" ( Top L)) by Th34

      .= (a "\/" b) by WAYBEL_1: 4;

    end;

    theorem :: YELLOW_5:52

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

    proof



      thus ((a "/\" b) "\/" (a \ b)) = (((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" ( 'not' b))) by Th17

      .= (a "/\" ((a "/\" b) "\/" ( 'not' b))) by LATTICE3: 17

      .= (a "/\" ((( 'not' b) "\/" a) "/\" (( 'not' b) "\/" b))) by Th17

      .= (a "/\" ((( 'not' b) "\/" a) "/\" ( Top L))) by Th34

      .= (a "/\" (( 'not' b) "\/" a)) by WAYBEL_1: 4

      .= a by LATTICE3: 18;

    end;

    theorem :: YELLOW_5:53

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

    proof



      thus (a \ (b \ c)) = (a "/\" (( 'not' b) "\/" ( 'not' ( 'not' c)))) by Th36

      .= (a "/\" (( 'not' b) "\/" c)) by WAYBEL_1: 87

      .= ((a \ b) "\/" (a "/\" c)) by WAYBEL_1:def 3;

    end;

    theorem :: YELLOW_5:54

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

    proof



      thus (a \ (a \ b)) = (a "/\" (( 'not' a) "\/" ( 'not' ( 'not' b)))) by Th36

      .= (a "/\" (( 'not' a) "\/" b)) by WAYBEL_1: 87

      .= ((a "/\" ( 'not' a)) "\/" (a "/\" b)) by WAYBEL_1:def 3

      .= (( Bottom L) "\/" (a "/\" b)) by Th34

      .= (a "/\" b) by WAYBEL_1: 3;

    end;

    theorem :: YELLOW_5:55

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

    proof



      thus ((a "\/" b) \ b) = ((a "\/" b) "/\" ( 'not' b))

      .= ((a "/\" ( 'not' b)) "\/" (b "/\" ( 'not' b))) by WAYBEL_1:def 3

      .= ((a "/\" ( 'not' b)) "\/" ( Bottom L)) by Th34

      .= (a \ b) by WAYBEL_1: 3;

    end;

    theorem :: YELLOW_5:56

    (a "/\" b) = ( Bottom L) iff (a \ b) = a

    proof

      thus (a "/\" b) = ( Bottom L) implies (a \ b) = a

      proof

        assume (a "/\" b) = ( Bottom L);

        then a <= ( 'not' b) by WAYBEL_1: 82;

        then (a "/\" a) <= (a "/\" ( 'not' b)) by Th6;

        then

         A1: a <= (a "/\" ( 'not' b)) by Th2;

        (a \ b) <= a by YELLOW_0: 23;

        hence thesis by A1, YELLOW_0:def 3;

      end;

      thus (a \ b) = a implies (a "/\" b) = ( Bottom L)

      proof

        assume (a \ b) = a;

        then (( 'not' a) "\/" ( 'not' ( 'not' b))) = ( 'not' a) by Th36;

        then (a "/\" (( 'not' a) "\/" b)) <= (a "/\" ( 'not' a)) by WAYBEL_1: 87;

        then ((a "/\" ( 'not' a)) "\/" (a "/\" b)) <= (a "/\" ( 'not' a)) by WAYBEL_1:def 3;

        then (( Bottom L) "\/" (a "/\" b)) <= (a "/\" ( 'not' a)) by Th34;

        then (( Bottom L) "\/" (a "/\" b)) <= ( Bottom L) by Th34;

        then

         A2: (a "/\" b) <= ( Bottom L) by WAYBEL_1: 3;

        ( Bottom L) <= (a "/\" b) by YELLOW_0: 44;

        hence thesis by A2, YELLOW_0:def 3;

      end;

    end;

    theorem :: YELLOW_5:57

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

    proof



      thus (a \ (b "\/" c)) = (a "/\" (( 'not' b) "/\" ( 'not' c))) by Th36

      .= ((a "/\" a) "/\" (( 'not' b) "/\" ( 'not' c))) by Th2

      .= (((a "/\" a) "/\" ( 'not' b)) "/\" ( 'not' c)) by LATTICE3: 16

      .= ((a "/\" (a "/\" ( 'not' b))) "/\" ( 'not' c)) by LATTICE3: 16

      .= ((a \ b) "/\" (a \ c)) by LATTICE3: 16;

    end;

    theorem :: YELLOW_5:58

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

    proof



      thus (a \ (b "/\" c)) = (a "/\" (( 'not' b) "\/" ( 'not' c))) by Th36

      .= ((a \ b) "\/" (a \ c)) by WAYBEL_1:def 3;

    end;

    theorem :: YELLOW_5:59

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

    proof



      thus ((a "/\" b) \ (a "/\" c)) = ((a "/\" b) "/\" (( 'not' a) "\/" ( 'not' c))) by Th36

      .= (((a "/\" b) "/\" ( 'not' a)) "\/" ((a "/\" b) "/\" ( 'not' c))) by WAYBEL_1:def 3

      .= (((a "/\" ( 'not' a)) "/\" b) "\/" ((a "/\" b) "/\" ( 'not' c))) by LATTICE3: 16

      .= ((( Bottom L) "/\" b) "\/" ((a "/\" b) "/\" ( 'not' c))) by Th34

      .= (( Bottom L) "\/" ((a "/\" b) "/\" ( 'not' c))) by WAYBEL_1: 3

      .= ((a "/\" b) "/\" ( 'not' c)) by WAYBEL_1: 3

      .= (a "/\" (b \ c)) by LATTICE3: 16;

    end;

    theorem :: YELLOW_5:60

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

    proof



      thus ((a "\/" b) \ (a "/\" b)) = ((a "\/" b) "/\" (( 'not' a) "\/" ( 'not' b))) by Th36

      .= (((a "\/" b) "/\" ( 'not' a)) "\/" ((a "\/" b) "/\" ( 'not' b))) by WAYBEL_1:def 3

      .= (((a "/\" ( 'not' a)) "\/" (b "/\" ( 'not' a))) "\/" ((a "\/" b) "/\" ( 'not' b))) by WAYBEL_1:def 3

      .= ((( Bottom L) "\/" (b "/\" ( 'not' a))) "\/" ((a "\/" b) "/\" ( 'not' b))) by Th34

      .= ((b \ a) "\/" ((a "\/" b) "/\" ( 'not' b))) by WAYBEL_1: 3

      .= ((b \ a) "\/" ((a "/\" ( 'not' b)) "\/" (b "/\" ( 'not' b)))) by WAYBEL_1:def 3

      .= ((b \ a) "\/" ((a "/\" ( 'not' b)) "\/" ( Bottom L))) by Th34

      .= ((a \ b) "\/" (b \ a)) by WAYBEL_1: 3;

    end;

    theorem :: YELLOW_5:61

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

    proof



      thus ((a \ b) \ c) = (a "/\" (( 'not' b) "/\" ( 'not' c))) by LATTICE3: 16

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

    end;

    theorem :: YELLOW_5:62



     Th62: ( 'not' ( Bottom L)) = ( Top L)

    proof

      (( Bottom L) "/\" ( Top L)) = ( Bottom L) & (( Bottom L) "\/" ( Top L)) = ( Top L) by WAYBEL_1: 3;

      then ( Top L) is_a_complement_of ( Bottom L) by WAYBEL_1:def 23;

      hence thesis by Th11;

    end;

    theorem :: YELLOW_5:63

    ( 'not' ( Top L)) = ( Bottom L)

    proof

      (( Bottom L) "/\" ( Top L)) = ( Bottom L) & (( Bottom L) "\/" ( Top L)) = ( Top L) by WAYBEL_1: 3;

      then ( Bottom L) is_a_complement_of ( Top L) by WAYBEL_1:def 23;

      hence thesis by Th11;

    end;

    theorem :: YELLOW_5:64

    (a \ a) = ( Bottom L) by Th34;

    theorem :: YELLOW_5:65

    (a \ ( Bottom L)) = a

    proof



      thus (a \ ( Bottom L)) = (a "/\" ( Top L)) by Th62

      .= a by WAYBEL_1: 4;

    end;

    theorem :: YELLOW_5:66

    ( 'not' (a \ b)) = (( 'not' a) "\/" b)

    proof



      thus ( 'not' (a \ b)) = (( 'not' a) "\/" ( 'not' ( 'not' b))) by Th36

      .= (( 'not' a) "\/" b) by WAYBEL_1: 87;

    end;

    theorem :: YELLOW_5:67

    (a "/\" b) misses (a \ b)

    proof

      ((a "/\" b) "/\" (a \ b)) = (((a "/\" b) "/\" ( 'not' b)) "/\" a) by LATTICE3: 16

      .= ((a "/\" (b "/\" ( 'not' b))) "/\" a) by LATTICE3: 16

      .= ((a "/\" ( Bottom L)) "/\" a) by Th34

      .= (( Bottom L) "/\" a) by WAYBEL_1: 3

      .= ( Bottom L) by WAYBEL_1: 3;

      hence thesis;

    end;

    theorem :: YELLOW_5:68

    (a \ b) misses b

    proof

      ((a \ b) "/\" b) = (a "/\" (( 'not' b) "/\" b)) by LATTICE3: 16

      .= (a "/\" ( Bottom L)) by Th34

      .= ( Bottom L) by WAYBEL_1: 3;

      hence thesis;

    end;

    theorem :: YELLOW_5:69

    a misses b implies ((a "\/" b) \ b) = a

    proof

      assume a misses b;

      then (a "/\" b) = ( Bottom L);

      then ((a "\/" ( 'not' b)) "/\" (b "\/" ( 'not' b))) <= (( Bottom L) "\/" ( 'not' b)) by Th17;

      then ((a "\/" ( 'not' b)) "/\" (b "\/" ( 'not' b))) <= ( 'not' b) by WAYBEL_1: 3;

      then ((a "\/" ( 'not' b)) "/\" ( Top L)) <= ( 'not' b) by Th34;

      then

       A1: (a "\/" ( 'not' b)) <= ( 'not' b) by WAYBEL_1: 4;

      ( 'not' b) <= (a "\/" ( 'not' b)) by YELLOW_0: 22;

      then (a "\/" ( 'not' b)) = ( 'not' b) by A1, YELLOW_0:def 3;

      then

       A2: a <= ( 'not' b) by YELLOW_0: 22;

      ((a "\/" b) \ b) = ((a "\/" b) "/\" ( 'not' b))

      .= ((a "/\" ( 'not' b)) "\/" (b "/\" ( 'not' b))) by WAYBEL_1:def 3

      .= ((a "/\" ( 'not' b)) "\/" ( Bottom L)) by Th34

      .= (a "/\" ( 'not' b)) by WAYBEL_1: 3

      .= a by A2, Th10;

      hence thesis;

    end;