robbins3.miz

    begin

    definition

      let L be non empty \/-SemiLattStr;

      :: ROBBINS3:def1

      attr L is join-Associative means for x,y,z be Element of L holds (x "\/" (y "\/" z)) = (y "\/" (x "\/" z));

    end

    definition

      let L be non empty /\-SemiLattStr;

      :: ROBBINS3:def2

      attr L is meet-Associative means for x,y,z be Element of L holds (x "/\" (y "/\" z)) = (y "/\" (x "/\" z));

    end

    definition

      let L be non empty LattStr;

      :: ROBBINS3:def3

      attr L is meet-Absorbing means for x,y be Element of L holds (x "\/" (x "/\" y)) = x;

    end

    theorem :: ROBBINS3:1



     Th1: for L be non empty LattStr holds L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is meet-idempotent join-idempotent

    proof

      let L be non empty LattStr;

      assume

       A1: L is meet-Associative join-Associative meet-Absorbing join-absorbing;



       A2: for x be Element of L holds (x "\/" x) = x

      proof

        let a be Element of L;

        a = (a "\/" (a "/\" a)) by A1;

        hence thesis by A1;

      end;

      for x be Element of L holds (x "/\" x) = x

      proof

        let a be Element of L;

        a = (a "/\" (a "\/" a)) by A1;

        hence thesis by A1;

      end;

      hence thesis by A2, ROBBINS1:def 7, SHEFFER1:def 9;

    end;

    theorem :: ROBBINS3:2



     Th2: for L be non empty LattStr holds L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is meet-commutative join-commutative

    proof

      let L be non empty LattStr;

      assume

       A1: L is meet-Associative join-Associative meet-Absorbing join-absorbing;

      then

       A2: L is join-idempotent meet-idempotent by Th1;



       A3: for x,y be Element of L holds (x "/\" y) = (y "/\" x)

      proof

        let a,b be Element of L;

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

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

        .= (b "/\" (a "/\" (b "\/" (a "\/" a)))) by A2, ROBBINS1:def 7

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

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

        hence thesis;

      end;

      for x,y be Element of L holds (x "\/" y) = (y "\/" x)

      proof

        let a,b be Element of L;

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

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

        .= (b "\/" (a "\/" (b "/\" (a "/\" a)))) by A2, SHEFFER1:def 9

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

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

        hence thesis;

      end;

      hence thesis by A3;

    end;

    theorem :: ROBBINS3:3



     Th3: for L be non empty LattStr holds L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is meet-absorbing

    proof

      let L be non empty LattStr;

      assume

       A1: L is meet-Associative join-Associative meet-Absorbing join-absorbing;

      then

       A2: L is meet-commutative join-commutative by Th2;

      for x,y be Element of L holds ((x "/\" y) "\/" y) = y

      proof

        let a,b be Element of L;

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

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

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

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS3:4



     Th4: for L be non empty LattStr holds L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is meet-associative join-associative

    proof

      let L be non empty LattStr;

      assume

       A1: L is meet-Associative join-Associative meet-Absorbing join-absorbing;

      then

       A2: L is meet-commutative join-commutative by Th2;



       A3: for x,y,z be Element of L holds (x "\/" (y "\/" z)) = ((x "\/" y) "\/" z)

      proof

        let a,b,c be Element of L;

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

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

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

        hence thesis;

      end;

      for x,y,z be Element of L holds (x "/\" (y "/\" z)) = ((x "/\" y) "/\" z)

      proof

        let a,b,c be Element of L;

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

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

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

        hence thesis;

      end;

      hence thesis by A3;

    end;

    theorem :: ROBBINS3:5



     Th5: for L be non empty LattStr holds L is Lattice-like iff L is meet-Associative join-Associative meet-Absorbing join-absorbing

    proof

      let L be non empty LattStr;



       A1: L is Lattice-like implies L is meet-Associative join-Associative meet-Absorbing join-absorbing

      proof

        assume

         A2: L is Lattice-like;



         A3: for x,y,z be Element of L holds (x "/\" (y "/\" z)) = (y "/\" (x "/\" z))

        proof

          let a,b,c be Element of L;

          (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c) by A2, LATTICES:def 7

          .= ((b "/\" a) "/\" c) by A2, LATTICES:def 6

          .= (b "/\" (a "/\" c)) by A2, LATTICES:def 7;

          hence thesis;

        end;



         A4: for x,y be Element of L holds (x "\/" (x "/\" y)) = x

        proof

          let a,b be Element of L;

          a = ((b "/\" a) "\/" a) by A2, LATTICES:def 8

          .= ((a "/\" b) "\/" a) by A2, LATTICES:def 6

          .= (a "\/" (a "/\" b)) by A2, LATTICES:def 4;

          hence thesis;

        end;

        for x,y,z be Element of L holds (x "\/" (y "\/" z)) = (y "\/" (x "\/" z))

        proof

          let a,b,c be Element of L;

          (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c) by A2, LATTICES:def 5

          .= ((b "\/" a) "\/" c) by A2, LATTICES:def 4

          .= (b "\/" (a "\/" c)) by A2, LATTICES:def 5;

          hence thesis;

        end;

        hence thesis by A2, A3, A4;

      end;

      L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is Lattice-like by Th3, Th2, Th4;

      hence thesis by A1;

    end;

    registration

      cluster Lattice-like -> meet-Associative join-Associative meet-Absorbing for non empty LattStr;

      coherence by Th5;

      cluster meet-Associative join-Associative meet-Absorbing join-absorbing -> Lattice-like for non empty LattStr;

      coherence by Th5;

    end

    begin

    registration

      cluster OrderInvolutive -> Dneg for PartialOrdered non empty OrthoRelStr;

      coherence

      proof

        let L be PartialOrdered non empty OrthoRelStr;

        assume L is OrderInvolutive;

        then

        consider f be Function of L, L such that

         A1: f = the Compl of L and

         A2: f is Orderinvolutive by OPOSET_1:def 18;

        f is involutive antitone by A2, OPOSET_1:def 17;

        hence thesis by A1, OPOSET_1:def 3;

      end;

    end

    theorem :: ROBBINS3:6



     Th6: for L be Dneg non empty OrthoRelStr, x be Element of L holds ((x ` ) ` ) = x

    proof

      let L be Dneg non empty OrthoRelStr, x be Element of L;

      consider f be Function of L, L such that

       A1: f = the Compl of L and

       A2: f is involutive by OPOSET_1:def 3;

      (f . x) = (x ` ) & (f . (f . x)) = x by A1, A2, PARTIT_2:def 3, ROBBINS1:def 3;

      hence thesis by A1, ROBBINS1:def 3;

    end;

    theorem :: ROBBINS3:7



     Th7: for O be OrderInvolutive PartialOrdered non empty OrthoRelStr, x,y be Element of O holds x <= y implies (y ` ) <= (x ` )

    proof

      let O be OrderInvolutive PartialOrdered non empty OrthoRelStr, x,y be Element of O;

      assume

       A1: x <= y;

      consider f be Function of O, O such that

       A2: f = the Compl of O and

       A3: f is Orderinvolutive by OPOSET_1:def 18;

      f is involutive antitone by A3, OPOSET_1:def 17;

      then (f . x) >= (f . y) by A1, WAYBEL_9:def 1;

      then (x ` ) >= (f . y) by A2, ROBBINS1:def 3;

      hence thesis by A2, ROBBINS1:def 3;

    end;

    registration

      cluster with_infima with_suprema strict for PreOrthoPoset;

      existence

      proof

        take TrivOrthoRelStr ;

        thus thesis;

      end;

    end

    notation

      let L be non empty \/-SemiLattStr, x,y be Element of L;

      synonym x |_| y for x "\/" y;

    end

    notation

      let L be non empty /\-SemiLattStr, x,y be Element of L;

      synonym x |^| y for x "/\" y;

    end

    notation

      let L be non empty RelStr, x,y be Element of L;

      synonym x "|^|" y for x "/\" y;

      synonym x "|_|" y for x "\/" y;

    end

    begin

    definition

      struct ( \/-SemiLattStr, RelStr) \/-SemiLattRelStr (# the carrier -> set,

the L_join -> BinOp of the carrier,

the InternalRel -> Relation of the carrier #)

       attr strict strict;

    end

    definition

      struct ( /\-SemiLattStr, RelStr) /\-SemiLattRelStr (# the carrier -> set,

the L_meet -> BinOp of the carrier,

the InternalRel -> Relation of the carrier #)

       attr strict strict;

    end

    definition

      struct ( /\-SemiLattRelStr, \/-SemiLattRelStr, LattStr) LattRelStr (# the carrier -> set,

the L_join, L_meet -> BinOp of the carrier,

the InternalRel -> Relation of the carrier #)

       attr strict strict;

    end

    definition

      :: ROBBINS3:def4

      func TrivLattRelStr -> LattRelStr equals LattRelStr (# { 0 }, op2 , op2 , ( id { 0 }) #);

      coherence ;

    end

    registration

      cluster TrivLattRelStr -> 1 -element;

      coherence ;

    end

    registration

      cluster non empty for \/-SemiLattRelStr;

      existence

      proof

        take TrivLattRelStr ;

        thus thesis;

      end;

      cluster non empty for /\-SemiLattRelStr;

      existence

      proof

        take TrivLattRelStr ;

        thus thesis;

      end;

      cluster non empty for LattRelStr;

      existence

      proof

        take TrivLattRelStr ;

        thus thesis;

      end;

    end

    theorem :: ROBBINS3:8

    for R be non empty RelStr st the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is antisymmetric transitive holds R is reflexive antisymmetric transitive

    proof

      let r be non empty RelStr;

      set i = the InternalRel of r;

      set c = the carrier of r;

      assume that

       A1: i is_reflexive_in c and

       A2: i is antisymmetric transitive;



       A3: i is_transitive_in ( field i) by A2;



       A4: ( field i) = c by A1, PARTIT_2: 21;

      then i is_antisymmetric_in c by A2;

      hence thesis by A1, A4, A3, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

    end;

    registration

      cluster TrivLattRelStr -> reflexive;

      coherence

      proof

        set T = TrivLattRelStr ;

        set C = the carrier of T;

        set I = the InternalRel of T;

        ( field I) = C by PARTIT_2: 18;

        then I is_reflexive_in C by RELAT_2:def 9;

        hence thesis by ORDERS_2:def 2;

      end;

    end

    registration

      cluster antisymmetric reflexive transitive with_suprema with_infima for LattRelStr;

      existence

      proof

        take TrivLattRelStr ;

        thus thesis;

      end;

    end

    registration

      cluster TrivLattRelStr -> meet-Absorbing;

      coherence ;

    end



     Lm1: TrivLattRelStr is Lattice-like;

    registration

      cluster Lattice-like for non empty LattRelStr;

      existence by Lm1;

    end

    definition

      let L be Lattice;

      :: original: LattRel

      redefine

      func LattRel L -> Order of the carrier of L ;

      coherence

      proof



         A1: ( LattRel L) = { [p, q] where p be Element of L, q be Element of L : p [= q } by FILTER_1:def 8;

        ( LattRel L) c= [:the carrier of L, the carrier of L:]

        proof

          let x be object;

          assume x in ( LattRel L);

          then ex p,q be Element of L st x = [p, q] & p [= q by A1;

          hence thesis by ZFMISC_1: 87;

        end;

        then

        reconsider R = ( LattRel L) as Relation of the carrier of L;



         A2: R is_antisymmetric_in the carrier of L

        proof

          let x,y be object;

          assume x in the carrier of L & y in the carrier of L;

          then

          reconsider x9 = x, y9 = y as Element of L;

          assume [x, y] in R & [y, x] in R;

          then x9 [= y9 & y9 [= x9 by FILTER_1: 31;

          hence thesis by LATTICES: 8;

        end;



         A3: R is_transitive_in the carrier of L

        proof

          let x,y,z be object;

          assume x in the carrier of L & y in the carrier of L & z in the carrier of L;

          then

          reconsider x9 = x, y9 = y, z9 = z as Element of L;

          assume [x, y] in R & [y, z] in R;

          then x9 [= y9 & y9 [= z9 by FILTER_1: 31;

          then x9 [= z9 by LATTICES: 7;

          hence thesis by FILTER_1: 31;

        end;



         A4: R is_reflexive_in the carrier of L by FILTER_1: 31;

        then ( dom R) = the carrier of L & ( field R) = the carrier of L by ORDERS_1: 13;

        hence thesis by A4, A2, A3, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

      end;

    end

    begin

    definition

      struct ( LattRelStr, OrthoLattStr, OrthoRelStr) OrthoLattRelStr (# the carrier -> set,

the L_join, L_meet -> BinOp of the carrier,

the InternalRel -> Relation of the carrier,

the Compl -> UnOp of the carrier #)

       attr strict strict;

    end

    definition

      :: ROBBINS3:def5

      func TrivCLRelStr -> OrthoLattRelStr equals OrthoLattRelStr (# { 0 }, op2 , op2 , ( id { 0 }), op1 #);

      coherence ;

    end

    definition

      let L be non empty ComplStr;

      :: ROBBINS3:def6

      attr L is involutive means

      : Def6: for x be Element of L holds ((x ` ) ` ) = x;

    end

    definition

      let L be non empty ComplLLattStr;

      :: ROBBINS3:def7

      attr L is with_Top means

      : Def7: for x,y be Element of L holds (x |_| (x ` )) = (y |_| (y ` ));

    end

    registration

      cluster TrivOrtLat -> involutive with_Top;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster TrivCLRelStr -> 1 -element;

      coherence ;

    end

    registration

      cluster TrivCLRelStr -> reflexive;

      coherence

      proof

        for x be Element of TrivCLRelStr holds x <= x

        proof

          let x be Element of TrivCLRelStr ;

           [x, x] in ( id { {} }) by RELAT_1:def 10;

          hence thesis by ORDERS_2:def 5;

        end;

        hence thesis by YELLOW_0:def 1;

      end;

    end

    registration

      cluster TrivCLRelStr -> involutive with_Top;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster involutive with_Top de_Morgan Lattice-like for 1 -element OrthoLattStr;

      existence

      proof

        take TrivOrtLat ;

        thus thesis;

      end;

    end

    definition

      mode Ortholattice is involutive with_Top de_Morgan Lattice-like non empty OrthoLattStr;

    end

    begin

    theorem :: ROBBINS3:9



     Th9: for K,L be non empty LattStr st the LattStr of K = the LattStr of L & K is join-commutative holds L is join-commutative

    proof

      let K,L be non empty LattStr;

      assume that

       A1: the LattStr of K = the LattStr of L and

       A2: K is join-commutative;

      L is join-commutative

      proof

        let x,y be Element of L;

        reconsider x9 = x, y9 = y as Element of K by A1;

        (x9 |_| y9) = (y9 |_| x9) by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS3:10



     Th10: for K,L be non empty LattStr st the LattStr of K = the LattStr of L & K is meet-commutative holds L is meet-commutative

    proof

      let K,L be non empty LattStr;

      assume that

       A1: the LattStr of K = the LattStr of L and

       A2: K is meet-commutative;

      L is meet-commutative

      proof

        let x,y be Element of L;

        reconsider x9 = x, y9 = y as Element of K by A1;

        (x9 "/\" y9) = (y9 "/\" x9) by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS3:11



     Th11: for K,L be non empty LattStr st the LattStr of K = the LattStr of L & K is join-associative holds L is join-associative

    proof

      let K,L be non empty LattStr;

      assume that

       A1: the LattStr of K = the LattStr of L and

       A2: K is join-associative;

      L is join-associative

      proof

        let x,y,z be Element of L;

        reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;

        ((x9 |_| y9) |_| z9) = (x9 |_| (y9 |_| z9)) by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS3:12



     Th12: for K,L be non empty LattStr st the LattStr of K = the LattStr of L & K is meet-associative holds L is meet-associative

    proof

      let K,L be non empty LattStr;

      assume that

       A1: the LattStr of K = the LattStr of L and

       A2: K is meet-associative;

      L is meet-associative

      proof

        let x,y,z be Element of L;

        reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;

        ((x9 "/\" y9) "/\" z9) = (x9 "/\" (y9 "/\" z9)) by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS3:13



     Th13: for K,L be non empty LattStr st the LattStr of K = the LattStr of L & K is join-absorbing holds L is join-absorbing

    proof

      let K,L be non empty LattStr;

      assume that

       A1: the LattStr of K = the LattStr of L and

       A2: K is join-absorbing;

      L is join-absorbing

      proof

        let x,y be Element of L;

        reconsider x9 = x, y9 = y as Element of K by A1;

        (x9 "/\" (x9 "\/" y9)) = x9 by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS3:14



     Th14: for K,L be non empty LattStr st the LattStr of K = the LattStr of L & K is meet-absorbing holds L is meet-absorbing

    proof

      let K,L be non empty LattStr;

      assume that

       A1: the LattStr of K = the LattStr of L and

       A2: K is meet-absorbing;

      L is meet-absorbing

      proof

        let x,y be Element of L;

        reconsider x9 = x, y9 = y as Element of K by A1;

        ((x9 "/\" y9) "\/" y9) = y9 by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS3:15

    for K,L be non empty LattStr st the LattStr of K = the LattStr of L & K is Lattice-like holds L is Lattice-like by Th9, Th10, Th11, Th12, Th13, Th14;

    theorem :: ROBBINS3:16

    for L1,L2 be non empty \/-SemiLattStr st the \/-SemiLattStr of L1 = the \/-SemiLattStr of L2 holds for a1,b1 be Element of L1, a2,b2 be Element of L2 st a1 = a2 & b1 = b2 holds (a1 "\/" b1) = (a2 "\/" b2);

    theorem :: ROBBINS3:17

    for L1,L2 be non empty /\-SemiLattStr st the /\-SemiLattStr of L1 = the /\-SemiLattStr of L2 holds for a1,b1 be Element of L1, a2,b2 be Element of L2 st a1 = a2 & b1 = b2 holds (a1 "/\" b1) = (a2 "/\" b2);

    theorem :: ROBBINS3:18



     Th18: for K,L be non empty ComplStr, x be Element of K, y be Element of L st the Compl of K = the Compl of L & x = y holds (x ` ) = (y ` )

    proof

      let K,L be non empty ComplStr, x be Element of K, y be Element of L;

      assume the Compl of K = the Compl of L & x = y;



      then (x ` ) = (the Compl of L . y) by ROBBINS1:def 3

      .= (y ` ) by ROBBINS1:def 3;

      hence thesis;

    end;

    theorem :: ROBBINS3:19



     Th19: for K,L be non empty ComplLLattStr st the ComplLLattStr of K = the ComplLLattStr of L & K is with_Top holds L is with_Top

    proof

      let K,L be non empty ComplLLattStr;

      assume that

       A1: the ComplLLattStr of K = the ComplLLattStr of L and

       A2: K is with_Top;

      for x,y be Element of L holds (x |_| (x ` )) = (y |_| (y ` ))

      proof

        let x,y be Element of L;

        reconsider x9 = x, y9 = y as Element of K by A1;

        (x |_| (x ` )) = (x9 |_| (x9 ` )) by A1, Th18

        .= (y9 |_| (y9 ` )) by A2

        .= (y |_| (y ` )) by A1, Th18;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ROBBINS3:20



     Th20: for K,L be non empty OrthoLattStr st the OrthoLattStr of K = the OrthoLattStr of L & K is de_Morgan holds L is de_Morgan

    proof

      let K,L be non empty OrthoLattStr;

      assume that

       A1: the OrthoLattStr of K = the OrthoLattStr of L and

       A2: K is de_Morgan;

      for x,y be Element of L holds (x "/\" y) = (((x ` ) "\/" (y ` )) ` )

      proof

        let x,y be Element of L;

        reconsider x9 = x, y9 = y as Element of K by A1;



         A3: (x ` ) = (x9 ` ) & (y ` ) = (y9 ` ) by A1, Th18;

        (x "/\" y) = (x9 "/\" y9) by A1

        .= (((x9 ` ) "\/" (y9 ` )) ` ) by A2, ROBBINS1:def 23

        .= (((x ` ) "\/" (y ` )) ` ) by A1, A3, Th18;

        hence thesis;

      end;

      hence thesis by ROBBINS1:def 23;

    end;

    theorem :: ROBBINS3:21



     Th21: for K,L be non empty OrthoLattStr st the OrthoLattStr of K = the OrthoLattStr of L & K is involutive holds L is involutive

    proof

      let K,L be non empty OrthoLattStr;

      assume that

       A1: the OrthoLattStr of K = the OrthoLattStr of L and

       A2: K is involutive;

      for x be Element of L holds ((x ` ) ` ) = x

      proof

        let x be Element of L;

        reconsider x9 = x as Element of K by A1;

        (x ` ) = (x9 ` ) by A1, Th18;



        then ((x ` ) ` ) = ((x9 ` ) ` ) by A1, Th18

        .= x by A2;

        hence thesis;

      end;

      hence thesis;

    end;

    begin

    definition

      let R be RelStr;

      :: ROBBINS3:def8

      mode RelAugmentation of R -> LattRelStr means the RelStr of it = the RelStr of R;

      existence

      proof

        set A = the BinOp of the carrier of R;

        set L = LattRelStr (# the carrier of R, A, A, the InternalRel of R #);

        take L;

        thus thesis;

      end;

    end

    definition

      let R be LattStr;

      :: ROBBINS3:def9

      mode LatAugmentation of R -> LattRelStr means

      : Def9: the LattStr of it = the LattStr of R;

      existence

      proof

        set IR = the Relation of the carrier of R;

        set L = LattRelStr (# the carrier of R, the L_join of R, the L_meet of R, IR #);

        take L;

        thus thesis;

      end;

    end

    registration

      let L be non empty LattStr;

      cluster -> non empty for LatAugmentation of L;

      coherence

      proof

        let R be LatAugmentation of L;

         the LattStr of L = the LattStr of R by Def9;

        hence thesis;

      end;

    end

    registration

      let L be meet-associative non empty LattStr;

      cluster -> meet-associative for LatAugmentation of L;

      coherence

      proof

        let R be LatAugmentation of L;

         the LattStr of L = the LattStr of R by Def9;

        hence thesis by Th12;

      end;

    end

    registration

      let L be join-associative non empty LattStr;

      cluster -> join-associative for LatAugmentation of L;

      coherence

      proof

        let R be LatAugmentation of L;

         the LattStr of L = the LattStr of R by Def9;

        hence thesis by Th11;

      end;

    end

    registration

      let L be meet-commutative non empty LattStr;

      cluster -> meet-commutative for LatAugmentation of L;

      coherence

      proof

        let R be LatAugmentation of L;

         the LattStr of L = the LattStr of R by Def9;

        hence thesis by Th10;

      end;

    end

    registration

      let L be join-commutative non empty LattStr;

      cluster -> join-commutative for LatAugmentation of L;

      coherence

      proof

        let R be LatAugmentation of L;

         the LattStr of L = the LattStr of R by Def9;

        hence thesis by Th9;

      end;

    end

    registration

      let L be join-absorbing non empty LattStr;

      cluster -> join-absorbing for LatAugmentation of L;

      coherence

      proof

        let R be LatAugmentation of L;

         the LattStr of L = the LattStr of R by Def9;

        hence thesis by Th13;

      end;

    end

    registration

      let L be meet-absorbing non empty LattStr;

      cluster -> meet-absorbing for LatAugmentation of L;

      coherence

      proof

        let R be LatAugmentation of L;

         the LattStr of L = the LattStr of R by Def9;

        hence thesis by Th14;

      end;

    end

    definition

      let L be non empty \/-SemiLattRelStr;

      :: ROBBINS3:def10

      attr L is naturally_sup-generated means

      : Def10: for x,y be Element of L holds x <= y iff (x |_| y) = y;

    end

    definition

      let L be non empty /\-SemiLattRelStr;

      :: ROBBINS3:def11

      attr L is naturally_inf-generated means for x,y be Element of L holds x <= y iff (x |^| y) = x;

    end

    registration

      let L be Lattice;

      cluster naturally_sup-generated naturally_inf-generated Lattice-like for LatAugmentation of L;

      existence

      proof

        set R = ( LattRel L);

        set S = LattRelStr (# the carrier of L, the L_join of L, the L_meet of L, R #);

         the LattStr of L = the LattStr of S;

        then

        reconsider S as LatAugmentation of L by Def9;

        for x,y be Element of S holds x <= y iff (x |^| y) = x

        proof

          let x,y be Element of S;

          reconsider x9 = x, y9 = y as Element of L;

          hereby

            assume x <= y;

            then [x, y] in the InternalRel of S by ORDERS_2:def 5;

            then x9 [= y9 by FILTER_1: 31;

            then (x9 |^| y9) = x9 by LATTICES: 4;

            hence (x |^| y) = x;

          end;



           A1: (x9 |^| y9) = (x |^| y);

          assume (x |^| y) = x;

          then x9 [= y9 by A1, LATTICES: 4;

          then [x9, y9] in ( LattRel L) by FILTER_1: 31;

          hence thesis by ORDERS_2:def 5;

        end;

        then

         A2: S is naturally_inf-generated;

        for x,y be Element of S holds x <= y iff (x |_| y) = y

        proof

          let x,y be Element of S;

          reconsider x9 = x, y9 = y as Element of L;

          hereby

            assume x <= y;

            then [x, y] in the InternalRel of S by ORDERS_2:def 5;

            then x9 [= y9 by FILTER_1: 31;

            then (x9 |_| y9) = y9;

            hence (x |_| y) = y;

          end;

          assume (x |_| y) = y;

          then x9 [= y9;

          then [x9, y9] in ( LattRel L) by FILTER_1: 31;

          hence thesis by ORDERS_2:def 5;

        end;

        then S is naturally_sup-generated;

        hence thesis by A2;

      end;

    end

    registration

      cluster 1 -element reflexive for LattRelStr;

      existence

      proof

        take TrivLattRelStr ;

        thus thesis;

      end;

    end

    registration

      cluster 1 -element reflexive for OrthoLattRelStr;

      existence

      proof

        take TrivCLRelStr ;

        thus thesis;

      end;

    end

    registration

      cluster 1 -element reflexive for OrthoRelStr;

      existence

      proof

        take TrivOrthoRelStr ;

        thus thesis;

      end;

    end

    registration

      cluster -> involutive with_Top de_Morgan well-complemented for 1 -element OrthoLattStr;

      coherence

      proof

        let L be 1 -element OrthoLattStr;

        reconsider L9 = L as 1 -element OrthoLattStr;



         A1: for x be Element of L9 holds ((x ` ) ` ) = x by STRUCT_0:def 10;



         A2: for x be Element of L9 holds (x ` ) is_a_complement_of x by STRUCT_0:def 10;

        (for x,y be Element of L9 holds (x |_| (x ` )) = (y |_| (y ` ))) & for x,y be Element of L9 holds (x |^| y) = (((x ` ) |_| (y ` )) ` ) by STRUCT_0:def 10;

        hence thesis by A1, A2, ROBBINS1:def 10, ROBBINS1:def 23;

      end;

    end

    registration

      cluster -> OrderInvolutive Pure PartialOrdered for 1 -element reflexive OrthoRelStr;

      coherence

      proof

        let L be 1 -element reflexive OrthoRelStr;

        reconsider L9 = L as 1 -element reflexive OrthoRelStr;

        reconsider f = the Compl of L9 as Function of L9, L9;

        consider x be object such that

         A1: the carrier of L9 = {x} by ZFMISC_1: 131;

        f = ( id {x}) by A1, FUNCT_2: 51;

        then

         A2: f is involutive;

        then

         A3: L9 is Dneg by OPOSET_1:def 3;

        for z,y be Element of L9 st z <= y holds (f . z) >= (f . y)

        proof

          let z,y be Element of L9;

          assume z <= y;

          (f . z) = x & (f . y) = x by A1, FUNCT_2: 50;

          hence thesis by YELLOW_0:def 1;

        end;

        then f is antitone by WAYBEL_9:def 1;

        then f is Orderinvolutive by A2, OPOSET_1:def 17;

        hence thesis by A3, OPOSET_1:def 15, OPOSET_1:def 18;

      end;

    end

    registration

      cluster -> naturally_sup-generated naturally_inf-generated for 1 -element reflexive LattRelStr;

      coherence

      proof

        let L be 1 -element reflexive LattRelStr;

        reconsider L9 = L as 1 -element reflexive LattRelStr;

        (for x,y be Element of L9 holds x <= y iff (x |_| y) = y) & for x,y be Element of L9 holds x <= y iff (x |^| y) = x by STRUCT_0:def 10;

        hence thesis;

      end;

    end

    registration

      cluster with_infima with_suprema naturally_sup-generated naturally_inf-generated de_Morgan Lattice-like OrderInvolutive Pure PartialOrdered for non empty OrthoLattRelStr;

      existence

      proof

        take TrivCLRelStr ;

        thus thesis;

      end;

    end

    registration

      cluster with_infima with_suprema naturally_sup-generated naturally_inf-generated Lattice-like for non empty LattRelStr;

      existence

      proof

        take TrivLattRelStr ;

        thus thesis;

      end;

    end

    theorem :: ROBBINS3:22



     Th22: for L be naturally_sup-generated non empty LattRelStr, x,y be Element of L holds x <= y iff x [= y by Def10;

    theorem :: ROBBINS3:23



     Th23: for L be naturally_sup-generated Lattice-like non empty LattRelStr holds the RelStr of L = ( LattPOSet L)

    proof

      let L be naturally_sup-generated Lattice-like non empty LattRelStr;



       A1: for x,y be object holds [x, y] in the InternalRel of L iff [x, y] in ( LattRel L)

      proof

        let x,y be object;

        hereby

          assume

           A2: [x, y] in the InternalRel of L;

          then

          reconsider x9 = x, y9 = y as Element of L by ZFMISC_1: 87;

          x9 <= y9 by A2, ORDERS_2:def 5;

          then x9 [= y9 by Th22;

          hence [x, y] in ( LattRel L) by FILTER_1: 31;

        end;

        assume

         A3: [x, y] in ( LattRel L);

        then

        reconsider x9 = x, y9 = y as Element of L by ZFMISC_1: 87;

        x9 [= y9 by A3, FILTER_1: 31;

        then x9 <= y9 by Th22;

        hence thesis by ORDERS_2:def 5;

      end;

      ( LattPOSet L) = RelStr (# the carrier of L, ( LattRel L) #) by LATTICE3:def 2;

      hence thesis by A1, RELAT_1:def 2;

    end;

    registration

      cluster naturally_sup-generated Lattice-like -> with_infima with_suprema for non empty LattRelStr;

      coherence

      proof

        let L be non empty LattRelStr;

        assume L is naturally_sup-generated Lattice-like;

        then

        reconsider L9 = L as naturally_sup-generated Lattice-like non empty LattRelStr;

        ( LattPOSet L9) is with_suprema with_infima;

        then the RelStr of L9 is with_suprema with_infima by Th23;

        hence thesis by YELLOW_7: 14, YELLOW_7: 15;

      end;

    end

    begin

    definition

      let R be OrthoLattStr;

      :: ROBBINS3:def12

      mode CLatAugmentation of R -> OrthoLattRelStr means

      : Def12: the OrthoLattStr of it = the OrthoLattStr of R;

      existence

      proof

        set IR = the Relation of the carrier of R;

        set L = OrthoLattRelStr (# the carrier of R, the L_join of R, the L_meet of R, IR, the Compl of R #);

        take L;

        thus thesis;

      end;

    end

    registration

      let L be non empty OrthoLattStr;

      cluster -> non empty for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        hence thesis;

      end;

    end

    registration

      let L be meet-associative non empty OrthoLattStr;

      cluster -> meet-associative for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        then the LattStr of L = the LattStr of R;

        hence thesis by Th12;

      end;

    end

    registration

      let L be join-associative non empty OrthoLattStr;

      cluster -> join-associative for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        then the LattStr of L = the LattStr of R;

        hence thesis by Th11;

      end;

    end

    registration

      let L be meet-commutative non empty OrthoLattStr;

      cluster -> meet-commutative for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        then the LattStr of L = the LattStr of R;

        hence thesis by Th10;

      end;

    end

    registration

      let L be join-commutative non empty OrthoLattStr;

      cluster -> join-commutative for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        then the LattStr of L = the LattStr of R;

        hence thesis by Th9;

      end;

    end

    registration

      let L be meet-absorbing non empty OrthoLattStr;

      cluster -> meet-absorbing for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        then the LattStr of L = the LattStr of R;

        hence thesis by Th14;

      end;

    end

    registration

      let L be join-absorbing non empty OrthoLattStr;

      cluster -> join-absorbing for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        then the LattStr of L = the LattStr of R;

        hence thesis by Th13;

      end;

    end

    registration

      let L be with_Top non empty OrthoLattStr;

      cluster -> with_Top for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        then the ComplLLattStr of L = the ComplLLattStr of R;

        hence thesis by Th19;

      end;

    end

    registration

      let L be non empty Ortholattice;

      cluster naturally_sup-generated naturally_inf-generated Lattice-like for CLatAugmentation of L;

      existence

      proof

        set R = ( LattRel L);

        set S = OrthoLattRelStr (# the carrier of L, the L_join of L, the L_meet of L, R, the Compl of L #);

         the OrthoLattStr of L = the OrthoLattStr of S;

        then

        reconsider S as CLatAugmentation of L by Def12;

        for x,y be Element of S holds x <= y iff (x |^| y) = x

        proof

          let x,y be Element of S;

          reconsider x9 = x, y9 = y as Element of L;

          hereby

            assume x <= y;

            then [x9, y9] in the InternalRel of S by ORDERS_2:def 5;

            then x9 [= y9 by FILTER_1: 31;

            then (x9 |^| y9) = x9 by LATTICES: 4;

            hence (x |^| y) = x;

          end;



           A1: (x9 |^| y9) = (x |^| y);

          assume (x |^| y) = x;

          then x9 [= y9 by A1, LATTICES: 4;

          then [x9, y9] in ( LattRel L) by FILTER_1: 31;

          hence thesis by ORDERS_2:def 5;

        end;

        then

         A2: S is naturally_inf-generated;

        for x,y be Element of S holds x <= y iff (x |_| y) = y

        proof

          let x,y be Element of S;

          reconsider x9 = x, y9 = y as Element of L;

          hereby

            assume x <= y;

            then [x, y] in the InternalRel of S by ORDERS_2:def 5;

            then x9 [= y9 by FILTER_1: 31;

            then (x9 |_| y9) = y9;

            hence (x |_| y) = y;

          end;

          assume (x |_| y) = y;

          then x9 [= y9;

          then [x9, y9] in ( LattRel L) by FILTER_1: 31;

          hence thesis by ORDERS_2:def 5;

        end;

        then S is naturally_sup-generated;

        hence thesis by A2;

      end;

    end

    registration

      cluster involutive with_Top de_Morgan Lattice-like naturally_sup-generated well-complemented for non empty OrthoLattRelStr;

      existence

      proof

        take TrivCLRelStr ;

        thus thesis;

      end;

    end

    theorem :: ROBBINS3:24



     Th24: for L be with_infima with_suprema PartialOrdered non empty OrthoRelStr holds for x,y be Element of L holds x <= y implies y = (x "|_|" y) & x = (x "|^|" y)

    proof

      let L be with_infima with_suprema PartialOrdered non empty OrthoRelStr;

      let a,b be Element of L;

      assume

       A1: a <= b;

      then b = (b "|_|" a) by YELLOW_0: 24;

      hence thesis by A1, LATTICE3: 13, YELLOW_0: 25;

    end;

    definition

      let L be meet-commutative non empty /\-SemiLattStr, a,b be Element of L;

      :: original: |^|

      redefine

      func a |^| b;

      commutativity by LATTICES:def 6;

    end

    definition

      let L be join-commutative non empty \/-SemiLattStr, a,b be Element of L;

      :: original: |_|

      redefine

      func a |_| b;

      commutativity by LATTICES:def 4;

    end

    registration

      cluster meet-absorbing join-absorbing meet-commutative naturally_sup-generated -> reflexive for non empty LattRelStr;

      coherence

      proof

        let L be non empty LattRelStr;

        assume L is meet-absorbing join-absorbing meet-commutative naturally_sup-generated;

        then

        reconsider L9 = L as meet-absorbing join-absorbing meet-commutative naturally_sup-generated non empty LattRelStr;

        for x be Element of L9 holds x <= x

        proof

          let x be Element of L9;

          x [= x;

          hence thesis by Th22;

        end;

        hence thesis by YELLOW_0:def 1;

      end;

    end

    registration

      cluster join-associative naturally_sup-generated -> transitive for non empty LattRelStr;

      coherence

      proof

        let L be non empty LattRelStr;

        assume L is join-associative naturally_sup-generated;

        then

        reconsider L9 = L as join-associative naturally_sup-generated non empty LattRelStr;

        for x,y,z be Element of L9 st x <= y & y <= z holds x <= z

        proof

          let x,y,z be Element of L9;

          assume x <= y & y <= z;

          then x [= y & y [= z by Th22;

          then x [= z by LATTICES: 7;

          hence thesis by Th22;

        end;

        hence thesis by YELLOW_0:def 2;

      end;

    end

    registration

      cluster join-commutative naturally_sup-generated -> antisymmetric for non empty LattRelStr;

      coherence

      proof

        let L be non empty LattRelStr;

        assume L is join-commutative naturally_sup-generated;

        then

        reconsider L9 = L as join-commutative naturally_sup-generated non empty LattRelStr;

        for x,y be Element of L9 st x <= y & y <= x holds x = y

        proof

          let x,y be Element of L9;

          assume x <= y & y <= x;

          then x [= y & y [= x by Th22;

          hence thesis by LATTICES: 8;

        end;

        hence thesis by YELLOW_0:def 3;

      end;

    end

    theorem :: ROBBINS3:25



     Th25: for L be with_infima with_suprema naturally_sup-generated Lattice-like non empty OrthoLattRelStr, x,y be Element of L holds (x "|_|" y) = (x |_| y)

    proof

      let L be with_infima with_suprema naturally_sup-generated Lattice-like non empty OrthoLattRelStr, x,y be Element of L;

      x <= (x "|_|" y) by YELLOW_0: 22;

      then

       A1: x [= (x "|_|" y) by Th22;

      y <= (x "|_|" y) by YELLOW_0: 22;

      then

       A2: y [= (x "|_|" y) by Th22;

      x [= (x |_| y) by LATTICES: 5;

      then

       A3: x <= (x |_| y) by Th22;

      y [= (x |_| y) by LATTICES: 5;

      then

       A4: y <= (x |_| y) by Th22;

      ((x |_| y) "|_|" (x "|_|" y)) = (((x |_| y) "|_|" x) "|_|" y) by LATTICE3: 14

      .= ((x |_| y) "|_|" y) by A3, YELLOW_0: 24

      .= (x |_| y) by A4, YELLOW_0: 24;

      then (x "|_|" y) <= (x |_| y) by YELLOW_0: 24;

      then

       A5: (x "|_|" y) [= (x |_| y) by Th22;

      ((x "|_|" y) |_| (x |_| y)) = (((x "|_|" y) |_| x) |_| y) by LATTICES:def 5

      .= ((x "|_|" y) |_| y) by A1

      .= (x "|_|" y) by A2;

      hence thesis by A5;

    end;

    theorem :: ROBBINS3:26



     Th26: for L be with_infima with_suprema naturally_sup-generated Lattice-like non empty OrthoLattRelStr, x,y be Element of L holds (x "|^|" y) = (x |^| y)

    proof

      let L be with_infima with_suprema naturally_sup-generated Lattice-like non empty OrthoLattRelStr, x,y be Element of L;

      (x "|^|" y) <= x by YELLOW_0: 23;

      then

       A1: (x "|^|" y) [= x by Th22;

      (x "|^|" y) <= y by YELLOW_0: 23;

      then

       A2: (x "|^|" y) [= y by Th22;

      (x |^| y) [= x by LATTICES: 6;

      then

       A3: (x |^| y) <= x by Th22;

      (x |^| y) [= y by LATTICES: 6;

      then

       A4: (x |^| y) <= y by Th22;

      ((x |^| y) "|^|" (x "|^|" y)) = (((x |^| y) "|^|" x) "|^|" y) by LATTICE3: 16

      .= ((x |^| y) "|^|" y) by A3, YELLOW_0: 25

      .= (x |^| y) by A4, YELLOW_0: 25;

      then (x |^| y) <= (x "|^|" y) by YELLOW_0: 25;

      then

       A5: (x |^| y) [= (x "|^|" y) by Th22;

      ((x "|^|" y) |^| (x |^| y)) = (((x "|^|" y) |^| x) |^| y) by LATTICES:def 7

      .= ((x "|^|" y) |^| y) by A1, LATTICES: 4

      .= (x "|^|" y) by A2, LATTICES: 4;

      hence thesis by A5, LATTICES: 4;

    end;

    theorem :: ROBBINS3:27

    for L be with_infima with_suprema naturally_sup-generated naturally_inf-generated Lattice-like OrderInvolutive PartialOrdered non empty OrthoLattRelStr holds L is de_Morgan

    proof

      let L be with_infima with_suprema naturally_sup-generated naturally_inf-generated Lattice-like OrderInvolutive PartialOrdered non empty OrthoLattRelStr;



       A1: for x,y be Element of L holds ((x ` ) "|_|" (y ` )) <= ((x "|^|" y) ` )

      proof

        let a,b be Element of L;

        set i = (a "|^|" b);

        set s = ((a ` ) "|_|" (b ` ));

        i <= a by YELLOW_0: 23;

        then (a ` ) <= (i ` ) by Th7;

        then

         A2: s <= ((i ` ) "|_|" (b ` )) by WAYBEL_1: 2;

        i <= b by YELLOW_0: 23;

        then (b ` ) <= (i ` ) by Th7;

        then (i ` ) = ((b ` ) "|_|" (i ` )) by Th24;

        hence thesis by A2, LATTICE3: 13;

      end;



       A3: for x,y be Element of L holds ((x "|_|" y) ` ) <= ((x ` ) "|^|" (y ` ))

      proof

        let a,b be Element of L;

        set i = ((a ` ) "|^|" (b ` ));

        set s = (a "|_|" b);

        a <= s by YELLOW_0: 22;

        then (s ` ) <= (a ` ) by Th7;

        then

         A4: ((s ` ) "|^|" (b ` )) <= i by WAYBEL_1: 1;

        b <= s by YELLOW_0: 22;

        then (s ` ) <= (b ` ) by Th7;

        hence thesis by A4, Th24;

      end;

      for x,y be Element of L holds (((x ` ) |_| (y ` )) ` ) = (x |^| y)

      proof

        let a,b be Element of L;

        set s = ((a ` ) "|_|" (b ` ));

        set i = (a "|^|" b);

        ((a ` ) ` ) = a & ((b ` ) ` ) = b by Th6;

        then

         A5: (s ` ) <= i by A3;

        ((i ` ) ` ) <= (s ` ) by A1, Th7;

        then

         A6: i <= (s ` ) by Th6;

        i = (a |^| b) & s = ((a ` ) |_| (b ` )) by Th25, Th26;

        hence thesis by A5, A6, ORDERS_2: 2;

      end;

      hence thesis by ROBBINS1:def 23;

    end;

    registration

      let L be Ortholattice;

      cluster -> involutive for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        hence thesis by Th21;

      end;

    end

    registration

      let L be Ortholattice;

      cluster -> de_Morgan for CLatAugmentation of L;

      coherence

      proof

        let R be CLatAugmentation of L;

         the OrthoLattStr of L = the OrthoLattStr of R by Def12;

        hence thesis by Th20;

      end;

    end

    theorem :: ROBBINS3:28



     Th28: for L be non empty OrthoLattRelStr st L is involutive with_Top de_Morgan Lattice-like naturally_sup-generated holds L is Orthocomplemented PartialOrdered

    proof

      let L be non empty OrthoLattRelStr;

      assume L is involutive with_Top de_Morgan Lattice-like naturally_sup-generated;

      then

      reconsider L9 = L as involutive with_Top de_Morgan Lattice-like naturally_sup-generated non empty OrthoLattRelStr;

      reconsider f = the Compl of L9 as Function of L9, L9;

      for x,y be Element of L9 st x <= y holds (f . x) >= (f . y)

      proof

        let x,y be Element of L9;

        assume x <= y;

        then x [= y by Th22;



        then

         A1: (x ` ) = ((x |^| y) ` ) by LATTICES: 4

        .= ((((x ` ) |_| (y ` )) ` ) ` ) by ROBBINS1:def 23

        .= ((x ` ) |_| (y ` )) by Def6;

        (f . x) = (x ` ) & (f . y) = (y ` ) by ROBBINS1:def 3;

        hence thesis by A1, Def10;

      end;

      then

       A2: f is antitone by WAYBEL_9:def 1;



       A3: for y be Element of L9 holds ex_sup_of ( {y, (f . y)},L9) & ex_inf_of ( {y, (f . y)},L9) & ( "\/" ( {y, (f . y)},L9)) is_maximum_of the carrier of L9 & ( "/\" ( {y, (f . y)},L9)) is_minimum_of the carrier of L9

      proof

        set xx = ( "\/" (the carrier of L9,L9));

        let y be Element of L9;

        thus ex_sup_of ( {y, (f . y)},L9) by YELLOW_0: 20;

        thus ex_inf_of ( {y, (f . y)},L9) by YELLOW_0: 21;

        set t = (y |_| (y ` ));

        for b be Element of L9 st b in the carrier of L9 holds b <= t

        proof

          let b be Element of L9;

          assume b in the carrier of L9;

          (b |_| (y |_| (y ` ))) = (b |_| (b |_| (b ` ))) by Def7

          .= ((b |_| b) |_| (b ` )) by LATTICES:def 5

          .= (b |_| (b ` ))

          .= (y |_| (y ` )) by Def7;

          then b [= t;

          hence thesis by Th22;

        end;

        then

         A4: t is_>=_than the carrier of L9 by LATTICE3:def 9;

        then L9 is upper-bounded by YELLOW_0:def 5;

        then

         A5: ex_sup_of (the carrier of L9,L9) by YELLOW_0: 43;

        reconsider t as Element of L9;



         A6: for a be Element of L9 st the carrier of L9 is_<=_than a holds t <= a by LATTICE3:def 9;

        ( "\/" ( {y, (f . y)},L9)) = ( "\/" ( {y, (y ` )},L9)) by ROBBINS1:def 3

        .= (y "|_|" (y ` )) by YELLOW_0: 41

        .= (y |_| (y ` )) by Th25

        .= xx by A4, A5, A6, YELLOW_0:def 9;

        hence ( "\/" ( {y, (f . y)},L9)) is_maximum_of the carrier of L9 by A5, WAYBEL_1:def 7;

        set xx = ( "/\" (the carrier of L9,L9));

        set t = (y |^| (y ` ));



         A7: for a,b be Element of L9 holds (a |^| (a ` )) = (b |^| (b ` ))

        proof

          let a,b be Element of L9;

          (a |^| (a ` )) = (((a ` ) |_| ((a ` ) ` )) ` ) by ROBBINS1:def 23

          .= (((b ` ) |_| ((b ` ) ` )) ` ) by Def7

          .= (b |^| (b ` )) by ROBBINS1:def 23;

          hence thesis;

        end;

        for b be Element of L9 st b in the carrier of L9 holds b >= t

        proof

          let b be Element of L9;

          assume b in the carrier of L9;

          (b |^| (y |^| (y ` ))) = (b |^| (b |^| (b ` ))) by A7

          .= ((b |^| b) |^| (b ` )) by LATTICES:def 7

          .= (b |^| (b ` ))

          .= (y |^| (y ` )) by A7;

          then t [= b by LATTICES: 4;

          hence thesis by Th22;

        end;

        then

         A8: t is_<=_than the carrier of L9 by LATTICE3:def 8;

        then L9 is lower-bounded by YELLOW_0:def 4;

        then

         A9: ex_inf_of (the carrier of L9,L9) by YELLOW_0: 42;

        reconsider t as Element of L9;



         A10: for a be Element of L9 st the carrier of L9 is_>=_than a holds t >= a by LATTICE3:def 8;

        ( "/\" ( {y, (f . y)},L9)) = ( "/\" ( {y, (y ` )},L9)) by ROBBINS1:def 3

        .= (y "|^|" (y ` )) by YELLOW_0: 40

        .= (y |^| (y ` )) by Th26

        .= xx by A8, A9, A10, YELLOW_0:def 10;

        hence thesis by A9, WAYBEL_1:def 6;

      end;

      for x be Element of L9 holds (f . (f . x)) = x

      proof

        let x be Element of L9;

        (f . (f . x)) = (f . (x ` )) by ROBBINS1:def 3

        .= ((x ` ) ` ) by ROBBINS1:def 3

        .= x by Def6;

        hence thesis;

      end;

      then f is involutive by PARTIT_2:def 3;

      then f is Orderinvolutive by A2, OPOSET_1:def 17;

      then f OrthoComplement_on L9 by A3, OPOSET_1:def 21;

      hence thesis by OPOSET_1:def 22;

    end;

    theorem :: ROBBINS3:29

    for L be Ortholattice, E be naturally_sup-generated CLatAugmentation of L holds E is Orthocomplemented by Th28;

    registration

      let L be Ortholattice;

      cluster -> Orthocomplemented for naturally_sup-generated CLatAugmentation of L;

      coherence by Th28;

    end

    theorem :: ROBBINS3:30



     Th30: for L be non empty OrthoLattStr st L is Boolean well-complemented Lattice-like holds L is Ortholattice

    proof

      let L be non empty OrthoLattStr;

      assume L is Boolean well-complemented Lattice-like;

      then

      reconsider L9 = L as Boolean well-complemented Lattice-like non empty OrthoLattStr;



       A1: for x,y be Element of L9 holds (x "/\" y) = (((x ` ) "\/" (y ` )) ` ) by ROBBINS1: 33;

      (for x be Element of L9 holds ((x ` ) ` ) = x) & for x,y be Element of L9 holds (x |_| (x ` )) = (y |_| (y ` )) by ROBBINS1: 3, ROBBINS1: 4;

      hence thesis by A1, Def6, Def7, ROBBINS1:def 23;

    end;

    registration

      cluster Boolean well-complemented Lattice-like -> involutive with_Top de_Morgan for non empty OrthoLattStr;

      coherence by Th30;

    end