:: ROBBINS4 semantic presentation

begin

registration
let L be Lattice;
cluster LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ->  Lattice-like ;
coherence
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is Lattice-like by ROBBINS3:15;
end;

theorem Th1: :: ROBBINS4:1
for K, L being Lattice st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) holds
LattPOSet K = LattPOSet L
proof
let K, L be Lattice; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) implies LattPOSet K = LattPOSet L )
assume A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ; ::_thesis: LattPOSet K = LattPOSet L
 for p, q being Element of K holds
( [p,q] in LattRel K iff [p,q] in LattRel L )
proof
let p, q be Element of K; ::_thesis: ( [p,q] in LattRel K iff [p,q] in LattRel L )
reconsider p9 = p, q9 = q as Element of L by A1;
hereby  ::_thesis: ( [p,q] in LattRel L implies [p,q] in LattRel K )
assume  [p,q] in LattRel K ; ::_thesis: [p,q] in LattRel L
then  p [= q by FILTER_1:31;
then  p "\/" q = q by LATTICES:def_3;
then  p9 "\/" q9 = q9 by A1;
then  p9 [= q9 by LATTICES:def_3;
hence  [p,q] in LattRel L by FILTER_1:31; ::_thesis: verum
end;
assume  [p,q] in LattRel L ; ::_thesis: [p,q] in LattRel K
then  p9 [= q9 by FILTER_1:31;
then  p9 "\/" q9 = q9 by LATTICES:def_3;
then  p "\/" q = q by A1;
then  p [= q by LATTICES:def_3;
hence  [p,q] in LattRel K by FILTER_1:31; ::_thesis: verum
end;
hence  LattPOSet K = LattPOSet L by A1, RELSET_1:def_2; ::_thesis: verum
end;

registration
cluster1 -element  -> 1 -element meet-Absorbing for OrthoLattStr ;
coherence
 for b1 being 1 -element OrthoLattStr holds b1 is meet-Absorbing ;
end;

registration
cluster non empty Lattice-like de_Morgan involutive with_Top  ->  lower-bounded for OrthoLattStr ;
coherence
 for b1 being Ortholattice holds b1 is lower-bounded
proof
let IT be Ortholattice; ::_thesis: IT is lower-bounded
 ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = c & a "/\" c = c )
proof
set x = the Element of IT;
take c = ((( the Element of IT `) `) "\/" ( the Element of IT `)) ` ; ::_thesis: for a being Element of IT holds
( c "/\" a = c & a "/\" c = c )
let a be Element of IT; ::_thesis: ( c "/\" a = c & a "/\" c = c )
thus c "/\" a = ((((a `) `) "\/" (a `)) `) "/\" a by ROBBINS3:def_7
.= ((a `) "/\" a) "/\" a by ROBBINS1:def_23
.= (a `) "/\" (a "/\" a) by LATTICES:def_7
.= (a `) "/\" a
.= (((a `) `) "\/" (a `)) ` by ROBBINS1:def_23
.= c by ROBBINS3:def_7 ; ::_thesis: a "/\" c = c
hence  a "/\" c = c ; ::_thesis: verum
end;
hence  IT is lower-bounded by LATTICES:def_13; ::_thesis: verum
end;
cluster non empty Lattice-like de_Morgan involutive with_Top  ->  upper-bounded for OrthoLattStr ;
coherence
 for b1 being Ortholattice holds b1 is upper-bounded
proof
let IT be Ortholattice; ::_thesis: IT is upper-bounded
 ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = c & a "\/" c = c )
proof
set x = the Element of IT;
take c = ( the Element of IT `) "\/" the Element of IT; ::_thesis: for a being Element of IT holds
( c "\/" a = c & a "\/" c = c )
let a be Element of IT; ::_thesis: ( c "\/" a = c & a "\/" c = c )
c "\/" a = ((a `) "\/" a) "\/" a by ROBBINS3:def_7
.= (a `) "\/" (a "\/" a) by LATTICES:def_5
.= (a `) "\/" a
.= c by ROBBINS3:def_7 ;
hence  ( c "\/" a = c & a "\/" c = c ) ; ::_thesis: verum
end;
hence  IT is upper-bounded by LATTICES:def_14; ::_thesis: verum
end;
end;


theorem Th2: :: ROBBINS4:2
for L being Ortholattice
for a being Element of L holds
( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L )
proof
let L be Ortholattice; ::_thesis: for a being Element of L holds
( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L )
let a be Element of L; ::_thesis: ( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L )
A1: for b being Element of L holds (a "\/" (a `)) "\/" b = a "\/" (a `)
proof
let b be Element of L; ::_thesis: (a "\/" (a `)) "\/" b = a "\/" (a `)
thus (a "\/" (a `)) "\/" b = (b "\/" (b `)) "\/" b by ROBBINS3:def_7
.= (b `) "\/" (b "\/" b) by LATTICES:def_5
.= (b `) "\/" b
.= a "\/" (a `) by ROBBINS3:def_7 ; ::_thesis: verum
end;
then  for b being Element of L holds b "\/" (a "\/" (a `)) = a "\/" (a `) ;
hence  a "\/" (a `) = Top L by A1, LATTICES:def_17; ::_thesis: a "/\" (a `) = Bottom L
A2: for b being Element of L holds (a "/\" (a `)) "/\" b = a "/\" (a `)
proof
let b be Element of L; ::_thesis: (a "/\" (a `)) "/\" b = a "/\" (a `)
thus (a "/\" (a `)) "/\" b = (((a `) "\/" ((a `) `)) `) "/\" b by ROBBINS1:def_23
.= (((b `) "\/" ((b `) `)) `) "/\" b by ROBBINS3:def_7
.= (b "/\" (b `)) "/\" b by ROBBINS1:def_23
.= (b `) "/\" (b "/\" b) by LATTICES:def_7
.= (b `) "/\" b
.= (((b `) `) "\/" (b `)) ` by ROBBINS1:def_23
.= (((a `) `) "\/" (a `)) ` by ROBBINS3:def_7
.= a "/\" (a `) by ROBBINS1:def_23 ; ::_thesis: verum
end;
then  for b being Element of L holds b "/\" (a "/\" (a `)) = a "/\" (a `) ;
hence  a "/\" (a `) = Bottom L by A2, LATTICES:def_16; ::_thesis: verum
end;

theorem Th3: :: ROBBINS4:3
for L being non empty OrthoLattStr holds
( L is Ortholattice iff ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) )
proof
let L be non empty OrthoLattStr ; ::_thesis: ( L is Ortholattice iff ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) )
thus  ( L is Ortholattice implies ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) ) ::_thesis: ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) implies L is Ortholattice )
proof
assume A1: L is Ortholattice ; ::_thesis: ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) )
thus  for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ::_thesis: ( ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) )
proof
let a, b, c be Element of L; ::_thesis: (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a
 (((c `) "/\" (b `)) `) "\/" a = (((((c `) `) "\/" ((b `) `)) `) `) "\/" a by A1, ROBBINS1:def_23;
then  (((c `) "/\" (b `)) `) "\/" a = (((c "\/" ((b `) `)) `) `) "\/" a by A1, ROBBINS3:def_6;
then  (((c `) "/\" (b `)) `) "\/" a = (((c "\/" b) `) `) "\/" a by A1, ROBBINS3:def_6;
then  (((c `) "/\" (b `)) `) "\/" a = (c "\/" b) "\/" a by A1, ROBBINS3:def_6;
then  (((c `) "/\" (b `)) `) "\/" a = a "\/" (c "\/" b) by A1, LATTICES:def_4;
then  (((c `) "/\" (b `)) `) "\/" a = c "\/" (a "\/" b) by A1, ROBBINS3:def_1;
hence  (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a by A1, LATTICES:def_4; ::_thesis: verum
end;
thus  for a, b being Element of L holds a = a "/\" (a "\/" b) by A1, LATTICES:def_9; ::_thesis: for a, b being Element of L holds a = a "\/" (b "/\" (b `))
let a, b be Element of L; ::_thesis: a = a "\/" (b "/\" (b `))
thus a "\/" (b "/\" (b `)) = a "\/" (((b `) "\/" ((b `) `)) `) by A1, ROBBINS1:def_23
.= a "\/" (((b `) "\/" b) `) by A1, ROBBINS3:def_6
.= a "\/" ((b "\/" (b `)) `) by A1, LATTICES:def_4
.= a "\/" ((a "\/" (a `)) `) by A1, ROBBINS3:def_7
.= a "\/" ((((a `) `) "\/" (a `)) `) by A1, ROBBINS3:def_6
.= a "\/" ((a `) "/\" a) by A1, ROBBINS1:def_23
.= ((a `) "/\" a) "\/" a by A1, LATTICES:def_4
.= a by A1, LATTICES:def_8 ; ::_thesis: verum
end;
assume A2: for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ; ::_thesis: ( ex a, b being Element of L st not a = a "/\" (a "\/" b) or ex a, b being Element of L st not a = a "\/" (b "/\" (b `)) or L is Ortholattice )
assume A3: for a, b being Element of L holds a = a "/\" (a "\/" b) ; ::_thesis: ( ex a, b being Element of L st not a = a "\/" (b "/\" (b `)) or L is Ortholattice )
assume A4: for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ; ::_thesis: L is Ortholattice
A5: for a being Element of L holds a "/\" a = a
proof
let a be Element of L; ::_thesis: a "/\" a = a
thus a "/\" a = a "/\" (a "\/" (a "/\" (a `))) by A4
.= a by A3 ; ::_thesis: verum
end;
A6: for a, b being Element of L holds a = (((b "/\" (b `)) `) `) "\/" a
proof
let a, b be Element of L; ::_thesis: a = (((b "/\" (b `)) `) `) "\/" a
set x = b "/\" (b `);
 (a "\/" (b "/\" (b `))) "\/" (b "/\" (b `)) = ((((b "/\" (b `)) `) "/\" ((b "/\" (b `)) `)) `) "\/" a by A2;
then  (a "\/" (b "/\" (b `))) "\/" (b "/\" (b `)) = (((b "/\" (b `)) `) `) "\/" a by A5;
then  a "\/" (b "/\" (b `)) = (((b "/\" (b `)) `) `) "\/" a by A4;
hence  a = (((b "/\" (b `)) `) `) "\/" a by A4; ::_thesis: verum
end;
A7: for a being Element of L holds a "/\" (a `) = ((a "/\" (a `)) `) `
proof
let a be Element of L; ::_thesis: a "/\" (a `) = ((a "/\" (a `)) `) `
set x = a "/\" (a `);
thus a "/\" (a `) = (((a "/\" (a `)) `) `) "\/" (a "/\" (a `)) by A6
.= ((a "/\" (a `)) `) ` by A4 ; ::_thesis: verum
end;
A8: for a, b being Element of L holds a = (b "/\" (b `)) "\/" a
proof
let a, b be Element of L; ::_thesis: a = (b "/\" (b `)) "\/" a
 a = (((b "/\" (b `)) `) `) "\/" a by A6;
hence  a = (b "/\" (b `)) "\/" a by A7; ::_thesis: verum
end;
A9: for a, b being Element of L holds a "\/" b = ((b `) "/\" (a `)) `
proof
let a, b be Element of L; ::_thesis: a "\/" b = ((b `) "/\" (a `)) `
set x = a "/\" (a `);
 ((a "/\" (a `)) "\/" a) "\/" b = (((b `) "/\" (a `)) `) "\/" (a "/\" (a `)) by A2;
hence a "\/" b = (((b `) "/\" (a `)) `) "\/" (a "/\" (a `)) by A8
.= ((b `) "/\" (a `)) ` by A4 ;
::_thesis: verum
end;
A10: L is involutive
proof
let a be Element of L; :: according to ROBBINS3:def_6 ::_thesis: (a `) ` = a
 ( a ` = (a `) "/\" ((a `) "\/" a) & (a `) "\/" a = ((a `) "/\" ((a `) `)) ` ) by A3, A9;
hence (a `) ` = ((a `) "/\" ((a `) `)) "\/" a by A9
.= a by A8 ;
::_thesis: verum
end;
A11: L is join-commutative
proof
let a, b be Element of L; :: according to LATTICES:def_4 ::_thesis: a "\/" b = b "\/" a
set x = a "/\" (a `);
 (a "/\" (a `)) "\/" b = ((b `) "/\" ((a "/\" (a `)) `)) ` by A9;
hence b "\/" a = (((b `) "/\" ((a "/\" (a `)) `)) `) "\/" a by A8
.= (a "\/" (a "/\" (a `))) "\/" b by A2
.= a "\/" b by A4 ;
::_thesis: verum
end;
A12: L is de_Morgan
proof
let a, b be Element of L; :: according to ROBBINS1:def_23 ::_thesis: a "/\" b = ((a `) "\/" (b `)) `
thus ((a `) "\/" (b `)) ` = ((b `) "\/" (a `)) ` by A11, LATTICES:def_4
.= ((((a `) `) "/\" ((b `) `)) `) ` by A9
.= ((a `) `) "/\" ((b `) `) by A10, ROBBINS3:def_6
.= ((a `) `) "/\" b by A10, ROBBINS3:def_6
.= a "/\" b by A10, ROBBINS3:def_6 ; ::_thesis: verum
end;
A13: L is meet-absorbing
proof
let a, b be Element of L; :: according to LATTICES:def_8 ::_thesis: (a "/\" b) "\/" b = b
thus (a "/\" b) "\/" b = ((b `) "/\" ((a "/\" b) `)) ` by A9
.= ((b `) "/\" ((((a `) "\/" (b `)) `) `)) ` by A12, ROBBINS1:def_23
.= ((b `) "/\" ((a `) "\/" (b `))) ` by A10, ROBBINS3:def_6
.= ((b `) "/\" ((b `) "\/" (a `))) ` by A11, LATTICES:def_4
.= (b `) ` by A3
.= b by A10, ROBBINS3:def_6 ; ::_thesis: verum
end;
A14: L is join-associative
proof
let a, b, c be Element of L; :: according to LATTICES:def_5 ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
thus (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a by A2
.= (b "\/" c) "\/" a by A9
.= a "\/" (b "\/" c) by A11, LATTICES:def_4 ; ::_thesis: verum
end;
A15: L is meet-associative
proof
let a, b, c be Element of L; :: according to LATTICES:def_7 ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
thus a "/\" (b "/\" c) = ((a `) "\/" ((b "/\" c) `)) ` by A12, ROBBINS1:def_23
.= ((a `) "\/" ((((b `) "\/" (c `)) `) `)) ` by A12, ROBBINS1:def_23
.= ((a `) "\/" ((b `) "\/" (c `))) ` by A10, ROBBINS3:def_6
.= (((a `) "\/" (b `)) "\/" (c `)) ` by A14, LATTICES:def_5
.= (((((a `) "\/" (b `)) `) `) "\/" (c `)) ` by A10, ROBBINS3:def_6
.= (((a "/\" b) `) "\/" (c `)) ` by A12, ROBBINS1:def_23
.= (a "/\" b) "/\" c by A12, ROBBINS1:def_23 ; ::_thesis: verum
end;
A16: for a, b being Element of L holds a "/\" (a `) = b "/\" (b `)
proof
let a, b be Element of L; ::_thesis: a "/\" (a `) = b "/\" (b `)
 a "/\" (a `) = (a "/\" (a `)) "\/" (b "/\" (b `)) by A4;
hence  a "/\" (a `) = b "/\" (b `) by A8; ::_thesis: verum
end;
A17: L is with_Top
proof
let a, b be Element of L; :: according to ROBBINS3:def_7 ::_thesis: a "\/" (a `) = b "\/" (b `)
 ((a `) "/\" ((a `) `)) ` = ((b `) "/\" ((b `) `)) ` by A16;
then  ((a `) "/\" ((a `) `)) ` = (b `) "\/" b by A9;
then  (a `) "\/" a = (b `) "\/" b by A9;
then  (a `) "\/" a = b "\/" (b `) by A11, LATTICES:def_4;
hence  a "\/" (a `) = b "\/" (b `) by A11, LATTICES:def_4; ::_thesis: verum
end;
 L is join-absorbing by A3, LATTICES:def_9;
hence  L is Ortholattice by A11, A14, A10, A12, A17, A15, A13; ::_thesis: verum
end;

theorem Th4: :: ROBBINS4:4
for L being non empty Lattice-like involutive OrthoLattStr holds
( L is de_Morgan iff for a, b being Element of L st a [= b holds
b ` [= a ` )
proof
let L be non empty Lattice-like involutive OrthoLattStr ; ::_thesis: ( L is de_Morgan iff for a, b being Element of L st a [= b holds
b ` [= a ` )
thus  ( L is de_Morgan implies for a, b being Element of L st a [= b holds
b ` [= a ` ) ::_thesis: ( ( for a, b being Element of L st a [= b holds
b ` [= a ` ) implies L is de_Morgan )
proof
assume A1: L is de_Morgan ; ::_thesis: for a, b being Element of L st a [= b holds
b ` [= a `
let a, b be Element of L; ::_thesis: ( a [= b implies b ` [= a ` )
assume  a [= b ; ::_thesis: b ` [= a `
then a ` = (a "/\" b) ` by LATTICES:4
.= (((a `) "\/" (b `)) `) ` by A1, ROBBINS1:def_23
.= (b `) "\/" (a `) by ROBBINS3:def_6 ;
then  (a `) "/\" (b `) = b ` by LATTICES:def_9;
hence  b ` [= a ` by LATTICES:4; ::_thesis: verum
end;
assume A2: for a, b being Element of L st a [= b holds
b ` [= a ` ; ::_thesis: L is de_Morgan
let x, y be Element of L; :: according to ROBBINS1:def_23 ::_thesis: x "/\" y = ((x `) "\/" (y `)) `
 ((x `) "\/" (y `)) ` [= (y `) ` by A2, LATTICES:5;
then A3: ((x `) "\/" (y `)) ` [= y by ROBBINS3:def_6;
 ( x ` [= (x "/\" y) ` & y ` [= (x "/\" y) ` ) by A2, LATTICES:6;
then  (x `) "\/" (y `) [= (x "/\" y) ` by FILTER_0:6;
then  ((x "/\" y) `) ` [= ((x `) "\/" (y `)) ` by A2;
then A4: x "/\" y [= ((x `) "\/" (y `)) ` by ROBBINS3:def_6;
 ((x `) "\/" (y `)) ` [= (x `) ` by A2, LATTICES:5;
then  ((x `) "\/" (y `)) ` [= x by ROBBINS3:def_6;
then  ((x `) "\/" (y `)) ` [= x "/\" y by A3, FILTER_0:7;
hence  x "/\" y = ((x `) "\/" (y `)) ` by A4, LATTICES:8; ::_thesis: verum
end;

begin

definition
let L be non empty OrthoLattStr ;
attrL is orthomodular  means :Def1: :: ROBBINS4:def 1
 for x, y being Element of L st x [= y holds
y = x "\/" ((x `) "/\" y);
end;

:: deftheorem Def1 defines orthomodular ROBBINS4:def_1_:_
 for L being non empty OrthoLattStr holds
( L is orthomodular iff for x, y being Element of L st x [= y holds
y = x "\/" ((x `) "/\" y) );

registration
cluster non empty trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like modular lower-bounded upper-bounded V147() Boolean de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top orthomodular for OrthoLattStr ;
existence
 ex b1 being Ortholattice st
( b1 is trivial & b1 is orthomodular & b1 is modular & b1 is Boolean )
proof
set L = the 1 -element Ortholattice;
 the 1 -element Ortholattice is orthomodular
proof
let x, y be Element of the 1 -element Ortholattice; :: according to ROBBINS4:def_1 ::_thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )
thus  ( x [= y implies y = x "\/" ((x `) "/\" y) ) by STRUCT_0:def_10; ::_thesis: verum
end;
hence  ex b1 being Ortholattice st
( b1 is trivial & b1 is orthomodular & b1 is modular & b1 is Boolean ) ; ::_thesis: verum
end;
end;

theorem Th5: :: ROBBINS4:5
for L being modular Ortholattice holds L is orthomodular
proof
let L be modular Ortholattice; ::_thesis: L is orthomodular
let x, y be Element of L; :: according to ROBBINS4:def_1 ::_thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )
assume  x [= y ; ::_thesis: y = x "\/" ((x `) "/\" y)
then  x "\/" ((x `) "/\" y) = (x "\/" (x `)) "/\" y by LATTICES:def_12;
then  x "\/" ((x `) "/\" y) = (y "\/" (y `)) "/\" y by ROBBINS3:def_7;
hence  y = x "\/" ((x `) "/\" y) by LATTICES:def_9; ::_thesis: verum
end;

definition
mode Orthomodular_Lattice is orthomodular Ortholattice;
end;

theorem Th6: :: ROBBINS4:6
for L being non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular OrthoLattStr
for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y
proof
let L be non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular OrthoLattStr ; ::_thesis: for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y
let x, y be Element of L; ::_thesis: x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y
 x [= x "\/" y by LATTICES:5;
hence  x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y by Def1; ::_thesis: verum
end;

definition
let L be non empty OrthoLattStr ;
attrL is Orthomodular  means :Def2: :: ROBBINS4:def 2
 for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y;
end;

:: deftheorem Def2 defines Orthomodular ROBBINS4:def_2_:_
 for L being non empty OrthoLattStr holds
( L is Orthomodular iff for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y );

registration
cluster non empty join-associative meet-commutative meet-absorbing join-absorbing Orthomodular  ->  non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular for OrthoLattStr ;
coherence
 for b1 being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b1 is Orthomodular holds
b1 is orthomodular
proof
let L be non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr ; ::_thesis: ( L is Orthomodular implies L is orthomodular )
assume A1: L is Orthomodular ; ::_thesis: L is orthomodular
let x, y be Element of L; :: according to ROBBINS4:def_1 ::_thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )
assume  x [= y ; ::_thesis: y = x "\/" ((x `) "/\" y)
then  x "\/" y = y by LATTICES:def_3;
hence  y = x "\/" ((x `) "/\" y) by A1, Def2; ::_thesis: verum
end;
cluster non empty join-associative meet-commutative meet-absorbing join-absorbing orthomodular  ->  non empty join-associative meet-commutative meet-absorbing join-absorbing Orthomodular for OrthoLattStr ;
coherence
 for b1 being non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr st b1 is orthomodular holds
b1 is Orthomodular
proof
let L be non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr ; ::_thesis: ( L is orthomodular implies L is Orthomodular )
assume  L is orthomodular ; ::_thesis: L is Orthomodular
then  for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y by Th6;
hence  L is Orthomodular by Def2; ::_thesis: verum
end;
end;

registration
cluster non empty Lattice-like modular de_Morgan involutive with_Top  ->  orthomodular for OrthoLattStr ;
coherence
 for b1 being Ortholattice st b1 is modular holds
b1 is orthomodular by Th5;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V147() de_Morgan join-Associative meet-Associative meet-Absorbing involutive with_Top orthomodular for OrthoLattStr ;
existence
 ex b1 being Ortholattice st
( b1 is join-Associative & b1 is meet-Absorbing & b1 is de_Morgan & b1 is orthomodular )
proof
set L = the 1 -element Ortholattice;
take  the 1 -element Ortholattice ; ::_thesis: ( the 1 -element Ortholattice is join-Associative & the 1 -element Ortholattice is meet-Absorbing & the 1 -element Ortholattice is de_Morgan & the 1 -element Ortholattice is orthomodular )
thus  ( the 1 -element Ortholattice is join-Associative & the 1 -element Ortholattice is meet-Absorbing & the 1 -element Ortholattice is de_Morgan & the 1 -element Ortholattice is orthomodular ) ; ::_thesis: verum
end;
end;

begin

definition
func B_6  ->  RelStr  equals :: ROBBINS4:def 3
 InclPoset {0,1,(3 \ 1),2,(3 \ 2),3};
coherence
 InclPoset {0,1,(3 \ 1),2,(3 \ 2),3} is RelStr ;
end;

:: deftheorem  defines B_6 ROBBINS4:def_3_:_
 B_6 = InclPoset {0,1,(3 \ 1),2,(3 \ 2),3};

registration
cluster B_6  ->  non empty ;
coherence
 not B_6 is empty ;
cluster B_6  ->  reflexive transitive antisymmetric ;
coherence
 ( B_6 is reflexive & B_6 is transitive & B_6 is antisymmetric ) ;
end;

Lm1:  3 \ 2 misses 2
by XBOOLE_1:79;

Lm2:  1 c= 2
by NAT_1:39;

then Lm3:  3 \ 2 misses 1
by Lm1, XBOOLE_1:63;

registration
cluster B_6  ->  with_suprema with_infima ;
coherence
 ( B_6 is with_suprema & B_6 is with_infima )
proof
set N = B_6 ;
set Z = {0,1,(3 \ 1),2,(3 \ 2),3};
A1: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A2: B_6 is with_suprema
proof
let x, y be Element of B_6; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of B_6 st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of B_6 holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
A3: {0,1,(3 \ 1),2,(3 \ 2),3} = the carrier of B_6 by YELLOW_1:1;
thus  ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) ) ::_thesis: verum
proof
percases ( ( x = 0 & y = 0 ) or ( x = 0 & y = 3 \ 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 \ 2 ) or ( x = 0 & y = 3 ) or ( x = 3 \ 1 & y = 0 ) or ( x = 3 \ 1 & y = 3 \ 1 ) or ( x = 3 \ 1 & y = 2 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 3 \ 1 ) or ( x = 1 & y = 3 \ 2 ) or ( x = 1 & y = 3 ) or ( x = 1 & y = 2 ) or ( y = 1 & x = 0 ) or ( y = 1 & x = 1 ) or ( y = 1 & x = 3 \ 1 ) or ( y = 1 & x = 3 \ 2 ) or ( y = 1 & x = 3 ) or ( y = 1 & x = 2 ) or ( x = 3 \ 1 & y = 3 \ 2 ) or ( x = 3 \ 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 3 \ 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 \ 2 ) or ( x = 2 & y = 3 ) or ( x = 3 \ 2 & y = 0 ) or ( x = 3 \ 2 & y = 3 \ 1 ) or ( x = 3 \ 2 & y = 2 ) or ( x = 3 \ 2 & y = 3 \ 2 ) or ( x = 3 \ 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 3 \ 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 \ 2 ) or ( x = 3 & y = 3 ) ) by A3, ENUMSET1:def_4;
suppose ( x = 0 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 0 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 0 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 0 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 0 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 1 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 1 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA4: ( x = 3 \ 1 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 3 in {0,1,(3 \ 1),2,(3 \ 2),3} by ENUMSET1:def_4;
then reconsider z = 3 as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 y c= z by A4, NAT_1:39;
hence  ( x <= z & y <= z ) by A4, YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let z9 be Element of B_6; ::_thesis: ( x <= z9 & y <= z9 implies z <= z9 )
assume that
A5: x <= z9 and
A6: y <= z9 ; ::_thesis: z <= z9
A7: z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A8: 3 \ 1 c= z9 by A4, A5, YELLOW_1:3;
A9: now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then A10: not 2 in z9 ;
 2 in 3 \ 1 by TARSKI:def_2, YELLOW11:3;
hence  contradiction by A8, A10; ::_thesis: verum
end;
A11: 2 c= z9 by A4, A6, YELLOW_1:3;
A12: now__::_thesis:_not_z9_=_3_\_1
A13: 0 in 2 by CARD_1:50, TARSKI:def_2;
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
hence  contradiction by A11, A13, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
A14: now__::_thesis:_not_z9_=_3_\_2
A15: 1 in 2 by CARD_1:50, TARSKI:def_2;
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
hence  contradiction by A11, A15, TARSKI:def_1, YELLOW11:4; ::_thesis: verum
end;
 ( z9 <> 1 & z9 <> 0 ) by A11, NAT_1:39;
hence  z <= z9 by A7, A12, A9, A14, ENUMSET1:def_4; ::_thesis: verum
end;
suppose ( x = 1 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 1 & y = 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA16: ( x = 1 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
A17: 1 c= 3 by NAT_1:39;
1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by A17, XBOOLE_1:12 ;
then reconsider z = x \/ y as Element of B_6 by A1, A16, ENUMSET1:def_4;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA18: ( x = 1 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 3 in {0,1,(3 \ 1),2,(3 \ 2),3} by ENUMSET1:def_4;
then reconsider z = 3 as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 x c= z by A18, NAT_1:39;
hence  ( x <= z & y <= z ) by A18, YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let z9 be Element of B_6; ::_thesis: ( x <= z9 & y <= z9 implies z <= z9 )
assume that
A19: x <= z9 and
A20: y <= z9 ; ::_thesis: z <= z9
A21: 3 \ 2 c= z9 by A18, A20, YELLOW_1:3;
A22: now__::_thesis:_not_z9_=_1
A23: 2 in 3 \ 2 by TARSKI:def_1, YELLOW11:4;
assume  z9 = 1 ; ::_thesis: contradiction
hence  contradiction by A21, A23, CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
A24: now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then A25: not 2 in z9 ;
 2 in 3 \ 2 by TARSKI:def_1, YELLOW11:4;
hence  contradiction by A21, A25; ::_thesis: verum
end;
A26: 1 c= z9 by A18, A19, YELLOW_1:3;
A27: now__::_thesis:_not_z9_=_3_\_1
A28: 0 in 1 by CARD_1:49, TARSKI:def_1;
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
hence  contradiction by A26, A28, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
A29: now__::_thesis:_not_z9_=_3_\_2
A30: 0 in 1 by CARD_1:49, TARSKI:def_1;
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
hence  contradiction by A26, A30, TARSKI:def_1, YELLOW11:4; ::_thesis: verum
end;
 ( z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} & z9 <> 0 ) by A26, YELLOW_1:1;
hence  z <= z9 by A27, A24, A29, A22, ENUMSET1:def_4; ::_thesis: verum
end;
supposeA31: ( x = 1 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 1 c= 3 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A31, XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA32: ( x = 1 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 1 c= 2 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A32, XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( y = 1 & x = 0 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( y = 1 & x = 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA33: ( y = 1 & x = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
A34: 1 c= 3 by NAT_1:39;
1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by A34, XBOOLE_1:12 ;
then reconsider z = x \/ y as Element of B_6 by A1, A33, ENUMSET1:def_4;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA35: ( y = 1 & x = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 3 in {0,1,(3 \ 1),2,(3 \ 2),3} by ENUMSET1:def_4;
then reconsider z = 3 as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 y c= z by A35, NAT_1:39;
hence  ( x <= z & y <= z ) by A35, YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let z9 be Element of B_6; ::_thesis: ( x <= z9 & y <= z9 implies z <= z9 )
assume that
A36: x <= z9 and
A37: y <= z9 ; ::_thesis: z <= z9
A38: 3 \ 2 c= z9 by A35, A36, YELLOW_1:3;
A39: now__::_thesis:_not_z9_=_1
A40: 2 in 3 \ 2 by TARSKI:def_1, YELLOW11:4;
assume  z9 = 1 ; ::_thesis: contradiction
hence  contradiction by A38, A40, CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
A41: now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then A42: not 2 in z9 ;
 2 in 3 \ 2 by TARSKI:def_1, YELLOW11:4;
hence  contradiction by A38, A42; ::_thesis: verum
end;
A43: 1 c= z9 by A35, A37, YELLOW_1:3;
A44: now__::_thesis:_not_z9_=_3_\_1
A45: 0 in 1 by CARD_1:49, TARSKI:def_1;
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
hence  contradiction by A43, A45, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
A46: now__::_thesis:_not_z9_=_3_\_2
A47: 0 in 1 by CARD_1:49, TARSKI:def_1;
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
hence  contradiction by A43, A47, TARSKI:def_1, YELLOW11:4; ::_thesis: verum
end;
 ( z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} & z9 <> 0 ) by A43, YELLOW_1:1;
hence  z <= z9 by A44, A41, A46, A39, ENUMSET1:def_4; ::_thesis: verum
end;
supposeA48: ( y = 1 & x = 3 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 1 c= 3 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A48, XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA49: ( y = 1 & x = 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 1 c= 2 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A49, XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 1 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 by Lm2, XBOOLE_1:12, XBOOLE_1:34;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 1 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 2 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA50: ( x = 2 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 3 in {0,1,(3 \ 1),2,(3 \ 2),3} by ENUMSET1:def_4;
then reconsider z = 3 as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 x c= z by A50, NAT_1:39;
hence  ( x <= z & y <= z ) by A50, YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let z9 be Element of B_6; ::_thesis: ( x <= z9 & y <= z9 implies z <= z9 )
assume that
A51: x <= z9 and
A52: y <= z9 ; ::_thesis: z <= z9
A53: z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A54: 3 \ 1 c= z9 by A50, A52, YELLOW_1:3;
A55: now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then A56: not 2 in z9 ;
 2 in 3 \ 1 by TARSKI:def_2, YELLOW11:3;
hence  contradiction by A54, A56; ::_thesis: verum
end;
A57: 2 c= z9 by A50, A51, YELLOW_1:3;
A58: now__::_thesis:_not_z9_=_3_\_1
A59: 0 in 2 by CARD_1:50, TARSKI:def_2;
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
hence  contradiction by A57, A59, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
A60: now__::_thesis:_not_z9_=_3_\_2
A61: 1 in 2 by CARD_1:50, TARSKI:def_2;
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
hence  contradiction by A57, A61, TARSKI:def_1, YELLOW11:4; ::_thesis: verum
end;
 ( z9 <> 1 & z9 <> 0 ) by A57, NAT_1:39;
hence  z <= z9 by A53, A58, A55, A60, ENUMSET1:def_4; ::_thesis: verum
end;
suppose ( x = 2 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA62: ( x = 2 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
A63: 2 c= 3 by NAT_1:39;
2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A63, XBOOLE_1:12 ;
then  x \/ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A62, ENUMSET1:def_4;
then reconsider z = x \/ y as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA64: ( x = 2 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 2 c= 3 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A64, XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 2 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 2 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 by Lm2, XBOOLE_1:12, XBOOLE_1:34;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA65: ( x = 3 \ 2 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
A66: 2 c= 3 by NAT_1:39;
2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A66, XBOOLE_1:12 ;
then  x \/ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A65, ENUMSET1:def_4;
then reconsider z = x \/ y as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 2 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 2 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
supposeA67: ( x = 3 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 2 c= 3 by NAT_1:39;
then reconsider z = x \/ y as Element of B_6 by A67, XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
then reconsider z = x \/ y as Element of B_6 ;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9 ) )
 ( x c= z & y c= z ) by XBOOLE_1:7;
hence  ( x <= z & y <= z ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds
z <= z9
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by YELLOW_1:3; ::_thesis: verum
end;
end;
end;
end;
 B_6 is with_infima
proof
let x, y be Element of B_6; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of B_6 st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of B_6 holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
A68: {0,1,(3 \ 1),2,(3 \ 2),3} = the carrier of B_6 by YELLOW_1:1;
thus  ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) ) ::_thesis: verum
proof
percases ( ( x = 0 & y = 0 ) or ( x = 0 & y = 3 \ 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 \ 2 ) or ( x = 0 & y = 3 ) or ( x = 3 \ 1 & y = 0 ) or ( x = 3 \ 1 & y = 3 \ 1 ) or ( x = 3 \ 1 & y = 2 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 3 \ 1 ) or ( x = 1 & y = 3 \ 2 ) or ( x = 1 & y = 3 ) or ( x = 1 & y = 2 ) or ( y = 1 & x = 0 ) or ( y = 1 & x = 1 ) or ( y = 1 & x = 3 \ 1 ) or ( y = 1 & x = 3 \ 2 ) or ( y = 1 & x = 3 ) or ( y = 1 & x = 2 ) or ( x = 3 \ 1 & y = 3 \ 2 ) or ( x = 3 \ 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 3 \ 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 \ 2 ) or ( x = 2 & y = 3 ) or ( x = 3 \ 2 & y = 0 ) or ( x = 3 \ 2 & y = 3 \ 1 ) or ( x = 3 \ 2 & y = 2 ) or ( x = 3 \ 2 & y = 3 \ 2 ) or ( x = 3 \ 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 3 \ 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 \ 2 ) or ( x = 3 & y = 3 ) ) by A68, ENUMSET1:def_4;
suppose ( x = 0 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 0 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 0 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 0 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 0 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 1 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 1 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA69: ( x = 3 \ 1 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 0 in {0,1,(3 \ 1),2,(3 \ 2),3} by ENUMSET1:def_4;
then reconsider z = 0 as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:2;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let z9 be Element of B_6; ::_thesis: ( z9 <= x & z9 <= y implies z9 <= z )
assume that
A70: z9 <= x and
A71: z9 <= y ; ::_thesis: z9 <= z
A72: z9 c= 3 \ 1 by A69, A70, YELLOW_1:3;
A73: now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then  0 in z9 by CARD_1:50, TARSKI:def_2;
hence  contradiction by A72, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
A74: z9 c= 2 by A69, A71, YELLOW_1:3;
A75: now__::_thesis:_not_z9_=_3_\_1
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
then A76: 2 in z9 by TARSKI:def_2, YELLOW11:3;
 not 2 in 2 ;
hence  contradiction by A74, A76; ::_thesis: verum
end;
A77: now__::_thesis:_not_z9_=_3
assume  z9 = 3 ; ::_thesis: contradiction
then A78: 2 in z9 by CARD_1:51, ENUMSET1:def_1;
 not 2 in 2 ;
hence  contradiction by A74, A78; ::_thesis: verum
end;
A79: now__::_thesis:_not_z9_=_3_\_2
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
then A80: 2 in z9 by TARSKI:def_1, YELLOW11:4;
 not 2 in 2 ;
hence  contradiction by A74, A80; ::_thesis: verum
end;
A81: now__::_thesis:_not_z9_=_1
assume  z9 = 1 ; ::_thesis: contradiction
then  0 in z9 by CARD_1:49, TARSKI:def_1;
hence  contradiction by A72, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
 z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
hence  z9 <= z by A75, A73, A79, A81, A77, ENUMSET1:def_4; ::_thesis: verum
end;
suppose ( x = 1 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 1 & y = 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 1 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then  x misses y by XBOOLE_1:79;
then  x /\ y = 0 by XBOOLE_0:def_7;
then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def_4;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 1 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then  x /\ y = 0 by Lm3, XBOOLE_0:def_7;
then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def_4;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA82: ( x = 1 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 1 c= 3 by NAT_1:39;
then reconsider z = x /\ y as Element of B_6 by A82, XBOOLE_1:28;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 1 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 by CARD_1:49, CARD_1:50, ZFMISC_1:13;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( y = 1 & x = 0 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( y = 1 & x = 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( y = 1 & x = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then  x misses y by XBOOLE_1:79;
then  x /\ y = 0 by XBOOLE_0:def_7;
then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def_4;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( y = 1 & x = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then  x /\ y = {} by Lm3, XBOOLE_0:def_7;
then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def_4;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA83: ( y = 1 & x = 3 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 1 c= 3 by NAT_1:39;
then reconsider z = x /\ y as Element of B_6 by A83, XBOOLE_1:28;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( y = 1 & x = 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 by CARD_1:49, CARD_1:50, ZFMISC_1:13;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 1 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 by YELLOW11:3, YELLOW11:4, ZFMISC_1:13;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA84: ( x = 3 \ 1 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
(3 \ 1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49
.= 3 \ 1 ;
then reconsider z = x /\ y as Element of B_6 by A84;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 2 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA85: ( x = 2 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 0 in {0,1,(3 \ 1),2,(3 \ 2),3} by ENUMSET1:def_4;
then reconsider z = 0 as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:2;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let z9 be Element of B_6; ::_thesis: ( z9 <= x & z9 <= y implies z9 <= z )
assume that
A86: z9 <= x and
A87: z9 <= y ; ::_thesis: z9 <= z
A88: z9 c= 3 \ 1 by A85, A87, YELLOW_1:3;
A89: now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then  0 in z9 by CARD_1:50, TARSKI:def_2;
hence  contradiction by A88, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
A90: z9 c= 2 by A85, A86, YELLOW_1:3;
A91: now__::_thesis:_not_z9_=_3_\_1
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
then A92: 2 in z9 by TARSKI:def_2, YELLOW11:3;
 not 2 in 2 ;
hence  contradiction by A90, A92; ::_thesis: verum
end;
A93: now__::_thesis:_not_z9_=_3
assume  z9 = 3 ; ::_thesis: contradiction
then A94: 2 in z9 by CARD_1:51, ENUMSET1:def_1;
 not 2 in 2 ;
hence  contradiction by A90, A94; ::_thesis: verum
end;
A95: now__::_thesis:_not_z9_=_3_\_2
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
then A96: 2 in z9 by TARSKI:def_1, YELLOW11:4;
 not 2 in 2 ;
hence  contradiction by A90, A96; ::_thesis: verum
end;
A97: now__::_thesis:_not_z9_=_1
assume  z9 = 1 ; ::_thesis: contradiction
then  0 in z9 by CARD_1:49, TARSKI:def_1;
hence  contradiction by A88, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
 z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
hence  z9 <= z by A91, A89, A95, A93, A97, ENUMSET1:def_4; ::_thesis: verum
end;
suppose ( x = 2 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA98: ( x = 2 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 2 misses 3 \ 2 by XBOOLE_1:79;
then  2 /\ (3 \ 2) = 0 by XBOOLE_0:def_7;
then  x /\ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A98, ENUMSET1:def_4;
then reconsider z = x /\ y as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA99: ( x = 2 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 2 c= 3 by NAT_1:39;
then reconsider z = x /\ y as Element of B_6 by A99, XBOOLE_1:28;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 2 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 2 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 by YELLOW11:3, YELLOW11:4, ZFMISC_1:13;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA100: ( x = 3 \ 2 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 2 misses 3 \ 2 by XBOOLE_1:79;
then  2 /\ (3 \ 2) = 0 by XBOOLE_0:def_7;
then  x /\ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A100, ENUMSET1:def_4;
then reconsider z = x /\ y as Element of B_6 by YELLOW_1:1;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 \ 2 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA101: ( x = 3 \ 2 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
(3 \ 2) /\ 3 = (3 /\ 3) \ 2 by XBOOLE_1:49
.= 3 \ 2 ;
then reconsider z = x /\ y as Element of B_6 by A101;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 & y = 0 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA102: ( x = 3 & y = 3 \ 1 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
(3 \ 1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49
.= 3 \ 1 ;
then reconsider z = x /\ y as Element of B_6 by A102;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA103: ( x = 3 & y = 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 2 c= 3 by NAT_1:39;
then reconsider z = x /\ y as Element of B_6 by A103, XBOOLE_1:28;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
supposeA104: ( x = 3 & y = 3 \ 2 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
(3 \ 2) /\ 3 = (3 /\ 3) \ 2 by XBOOLE_1:49
.= 3 \ 2 ;
then reconsider z = x /\ y as Element of B_6 by A104;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
suppose ( x = 3 & y = 3 ) ; ::_thesis: ex z being Element of B_6 st
( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
then reconsider z = x /\ y as Element of B_6 ;
take  z ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z ) )
 ( z c= x & z c= y ) by XBOOLE_1:17;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds
z9 <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by YELLOW_1:3; ::_thesis: verum
end;
end;
end;
end;
hence  ( B_6 is with_suprema & B_6 is with_infima ) by A2; ::_thesis: verum
end;
end;

theorem Th7: :: ROBBINS4:7
the carrier of (latt B_6) = {0,1,(3 \ 1),2,(3 \ 2),3}
proof
 RelStr(# the carrier of B_6, the InternalRel of B_6 #) = LattPOSet (latt B_6) by LATTICE3:def_15;
hence  the carrier of (latt B_6) = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1; ::_thesis: verum
end;

theorem Th8: :: ROBBINS4:8
for a being set st a in the carrier of (latt B_6) holds
a c= 3
proof
let a be set ; ::_thesis: ( a in the carrier of (latt B_6) implies a c= 3 )
assume  a in the carrier of (latt B_6) ; ::_thesis: a c= 3
then  ( a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 ) by Th7, ENUMSET1:def_4;
hence  a c= 3 by NAT_1:39; ::_thesis: verum
end;

definition
func Benzene  ->  strict OrthoLattStr  means :Def4: :: ROBBINS4:def 4
( LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = latt B_6 & ( for x being Element of it
for y being Subset of 3 st x = y holds
the Compl of it . x = y ` ) );
existence
 ex b1 being strict OrthoLattStr st
( LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = latt B_6 & ( for x being Element of b1
for y being Subset of 3 st x = y holds
the Compl of b1 . x = y ` ) )
proof
defpred S1[ set , set ] means  for y being Subset of 3 st $1 = y holds
$2 = y ` ;
set N = latt B_6;
set M = the carrier of (latt B_6);
set A = the L_join of (latt B_6);
set B = the L_meet of (latt B_6);
A1: for x being Element of the carrier of (latt B_6) ex y being Element of the carrier of (latt B_6) st S1[x,y]
proof
let x be Element of the carrier of (latt B_6); ::_thesis: ex y being Element of the carrier of (latt B_6) st S1[x,y]
reconsider z = x as Subset of 3 by Th8;
A2: 2 c= 3 by NAT_1:39;
A3: 1 c= 3 by NAT_1:39;
now__::_thesis:_z_`_in_the_carrier_of_(latt_B_6)
percases ( z = 0 or z = 1 or z = 3 \ 1 or z = 3 \ 2 or z = 2 or z = 3 ) by Th7, ENUMSET1:def_4;
suppose z = 0 ; ::_thesis: z ` in the carrier of (latt B_6)
hence  z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def_4; ::_thesis: verum
end;
suppose z = 1 ; ::_thesis: z ` in the carrier of (latt B_6)
hence  z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def_4; ::_thesis: verum
end;
suppose z = 3 \ 1 ; ::_thesis: z ` in the carrier of (latt B_6)
then z ` = 3 /\ 1 by XBOOLE_1:48
.= 1 by A3, XBOOLE_1:28 ;
hence  z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def_4; ::_thesis: verum
end;
suppose z = 3 \ 2 ; ::_thesis: z ` in the carrier of (latt B_6)
then z ` = 3 /\ 2 by XBOOLE_1:48
.= 2 by A2, XBOOLE_1:28 ;
hence  z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def_4; ::_thesis: verum
end;
suppose z = 2 ; ::_thesis: z ` in the carrier of (latt B_6)
hence  z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def_4; ::_thesis: verum
end;
suppose z = 3 ; ::_thesis: z ` in the carrier of (latt B_6)
then  z ` = 0 by XBOOLE_1:37;
hence  z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def_4; ::_thesis: verum
end;
end;
end;
then reconsider y = z ` as Element of the carrier of (latt B_6) ;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
 ex f being Function of the carrier of (latt B_6), the carrier of (latt B_6) st
for x being Element of the carrier of (latt B_6) holds S1[x,f . x] from FUNCT_2:sch_3(A1);
then consider C being UnOp of the carrier of (latt B_6) such that
A4: for x being Element of the carrier of (latt B_6)
for y being Subset of 3 st x = y holds
C . x = y ` ;
take  OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) ; ::_thesis: ( LattStr(# the carrier of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #), the L_join of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #), the L_meet of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) #) = latt B_6 & ( for x being Element of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #)
for y being Subset of 3 st x = y holds
the Compl of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) . x = y ` ) )
thus  ( LattStr(# the carrier of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #), the L_join of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #), the L_meet of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) #) = latt B_6 & ( for x being Element of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #)
for y being Subset of 3 st x = y holds
the Compl of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) . x = y ` ) ) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict OrthoLattStr st LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = latt B_6 & ( for x being Element of b1
for y being Subset of 3 st x = y holds
the Compl of b1 . x = y ` ) & LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = latt B_6 & ( for x being Element of b2
for y being Subset of 3 st x = y holds
the Compl of b2 . x = y ` ) holds
b1 = b2
proof
let A1, A2 be strict OrthoLattStr ; ::_thesis: ( LattStr(# the carrier of A1, the L_join of A1, the L_meet of A1 #) = latt B_6 & ( for x being Element of A1
for y being Subset of 3 st x = y holds
the Compl of A1 . x = y ` ) & LattStr(# the carrier of A2, the L_join of A2, the L_meet of A2 #) = latt B_6 & ( for x being Element of A2
for y being Subset of 3 st x = y holds
the Compl of A2 . x = y ` ) implies A1 = A2 )
assume that
A5: LattStr(# the carrier of A1, the L_join of A1, the L_meet of A1 #) = latt B_6 and
A6: for x being Element of A1
for y being Subset of 3 st x = y holds
the Compl of A1 . x = y ` and
A7: LattStr(# the carrier of A2, the L_join of A2, the L_meet of A2 #) = latt B_6 and
A8: for x being Element of A2
for y being Subset of 3 st x = y holds
the Compl of A2 . x = y ` ; ::_thesis: A1 = A2
set f2 = the Compl of A2;
set f1 = the Compl of A1;
set M = the carrier of A1;
 for x being Element of the carrier of A1 holds the Compl of A1 . x = the Compl of A2 . x
proof
let x be Element of the carrier of A1; ::_thesis: the Compl of A1 . x = the Compl of A2 . x
reconsider y = x as Subset of 3 by A5, Th8;
thus  the Compl of A1 . x = y ` by A6
.= the Compl of A2 . x by A5, A7, A8 ; ::_thesis: verum
end;
hence  A1 = A2 by A5, A7, FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Benzene ROBBINS4:def_4_:_
 for b1 being strict OrthoLattStr holds
( b1 = Benzene iff ( LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = latt B_6 & ( for x being Element of b1
for y being Subset of 3 st x = y holds
the Compl of b1 . x = y ` ) ) );

theorem Th9: :: ROBBINS4:9
the carrier of Benzene = {0,1,(3 \ 1),2,(3 \ 2),3}
proof
 ( LattStr(# the carrier of Benzene, the L_join of Benzene, the L_meet of Benzene #) = LattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6) #) & LattPOSet (latt B_6) = RelStr(# the carrier of B_6, the InternalRel of B_6 #) ) by Def4, LATTICE3:def_15;
hence  the carrier of Benzene = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1; ::_thesis: verum
end;

theorem Th10: :: ROBBINS4:10
the carrier of Benzene c= bool 3
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of Benzene or a in bool 3 )
A1: ( 0 c= 3 & 1 c= 3 ) by NAT_1:39;
assume A2: a in the carrier of Benzene ; ::_thesis: a in bool 3
A3: ( 2 c= 3 & 3 c= 3 ) by NAT_1:39;
 ( a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 ) by A2, Th9, ENUMSET1:def_4;
hence  a in bool 3 by A1, A3; ::_thesis: verum
end;

theorem Th11: :: ROBBINS4:11
for a being set st a in the carrier of Benzene holds
a c= {0,1,2} by Th10, CARD_1:51;

registration
cluster Benzene  ->  non empty strict ;
coherence
 not Benzene is empty by Th9;
cluster Benzene  ->  Lattice-like strict ;
coherence
 Benzene is Lattice-like
proof
 LattStr(# the carrier of Benzene, the L_join of Benzene, the L_meet of Benzene #) = latt B_6 by Def4;
hence  Benzene is Lattice-like by ROBBINS3:15; ::_thesis: verum
end;
end;

theorem Th12: :: ROBBINS4:12
LattPOSet LattStr(# the carrier of Benzene, the L_join of Benzene, the L_meet of Benzene #) = B_6
proof
 LattPOSet LattStr(# the carrier of Benzene, the L_join of Benzene, the L_meet of Benzene #) = LattPOSet (latt B_6) by Def4;
hence  LattPOSet LattStr(# the carrier of Benzene, the L_join of Benzene, the L_meet of Benzene #) = B_6 by LATTICE3:def_15; ::_thesis: verum
end;

theorem Th13: :: ROBBINS4:13
for a, b being Element of B_6
for x, y being Element of Benzene st a = x & b = y holds
( a <= b iff x [= y )
proof
let a, b be Element of B_6; ::_thesis: for x, y being Element of Benzene st a = x & b = y holds
( a <= b iff x [= y )
let x, y be Element of Benzene; ::_thesis: ( a = x & b = y implies ( a <= b iff x [= y ) )
assume A1: ( a = x & b = y ) ; ::_thesis: ( a <= b iff x [= y )
hereby  ::_thesis: ( x [= y implies a <= b )
assume  a <= b ; ::_thesis: x [= y
then  x % <= y % by A1, Th1, Th12;
hence  x [= y by LATTICE3:7; ::_thesis: verum
end;
assume  x [= y ; ::_thesis: a <= b
then  x % <= y % by LATTICE3:7;
hence  a <= b by A1, Th1, Th12; ::_thesis: verum
end;

theorem Th14: :: ROBBINS4:14
for a, b being Element of B_6
for x, y being Element of Benzene st a = x & b = y holds
( a "\/" b = x "\/" y & a "/\" b = x "/\" y )
proof
let a, b be Element of B_6; ::_thesis: for x, y being Element of Benzene st a = x & b = y holds
( a "\/" b = x "\/" y & a "/\" b = x "/\" y )
let x, y be Element of Benzene; ::_thesis: ( a = x & b = y implies ( a "\/" b = x "\/" y & a "/\" b = x "/\" y ) )
reconsider xy = x "\/" y as Element of B_6 by Th9, YELLOW_1:1;
assume that
A1: a = x and
A2: b = y ; ::_thesis: ( a "\/" b = x "\/" y & a "/\" b = x "/\" y )
 x [= x "\/" y by LATTICES:5;
then A3: a <= xy by A1, Th13;
A4: for d being Element of B_6 st d >= a & d >= b holds
xy <= d
proof
let d be Element of B_6; ::_thesis: ( d >= a & d >= b implies xy <= d )
reconsider e = d as Element of Benzene by Th9, YELLOW_1:1;
assume  ( d >= a & d >= b ) ; ::_thesis: xy <= d
then  ( x [= e & y [= e ) by A1, A2, Th13;
then  x "\/" y [= e by FILTER_0:6;
hence  xy <= d by Th13; ::_thesis: verum
end;
 y [= x "\/" y by LATTICES:5;
then A5: b <= xy by A2, Th13;
reconsider xy = x "/\" y as Element of B_6 by Th9, YELLOW_1:1;
 x "/\" y [= y by LATTICES:6;
then A6: xy <= b by A2, Th13;
A7: for d being Element of B_6 st d <= a & d <= b holds
xy >= d
proof
let d be Element of B_6; ::_thesis: ( d <= a & d <= b implies xy >= d )
reconsider e = d as Element of Benzene by Th9, YELLOW_1:1;
assume  ( d <= a & d <= b ) ; ::_thesis: xy >= d
then  ( e [= x & e [= y ) by A1, A2, Th13;
then  e [= x "/\" y by FILTER_0:7;
hence  xy >= d by Th13; ::_thesis: verum
end;
 x "/\" y [= x by LATTICES:6;
then  xy <= a by A1, Th13;
hence  ( a "\/" b = x "\/" y & a "/\" b = x "/\" y ) by A3, A5, A4, A6, A7, YELLOW_0:22, YELLOW_0:23; ::_thesis: verum
end;

theorem Th15: :: ROBBINS4:15
for a, b being Element of B_6 st a = 3 \ 1 & b = 2 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof
 ( 3 in {0,1,(3 \ 1),2,(3 \ 2),3} & 0 in {0,1,(3 \ 1),2,(3 \ 2),3} ) by ENUMSET1:def_4;
then reconsider t = 3, z = 0 as Element of B_6 by YELLOW_1:1;
let a, b be Element of B_6; ::_thesis: ( a = 3 \ 1 & b = 2 implies ( a "\/" b = 3 & a "/\" b = 0 ) )
assume that
A1: a = 3 \ 1 and
A2: b = 2 ; ::_thesis: ( a "\/" b = 3 & a "/\" b = 0 )
 b c= t by A2, NAT_1:39;
then A3: b <= t by YELLOW_1:3;
A4: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A5: for d being Element of B_6 st d >= a & d >= b holds
t <= d
proof
let z9 be Element of B_6; ::_thesis: ( z9 >= a & z9 >= b implies t <= z9 )
assume that
A6: z9 >= a and
A7: z9 >= b ; ::_thesis: t <= z9
A8: 2 c= z9 by A2, A7, YELLOW_1:3;
A9: now__::_thesis:_not_z9_=_3_\_1
A10: 0 in 2 by CARD_1:50, TARSKI:def_2;
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
hence  contradiction by A8, A10, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
A11: 3 \ 1 c= z9 by A1, A6, YELLOW_1:3;
A12: now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then A13: not 2 in z9 ;
 2 in 3 \ 1 by TARSKI:def_2, YELLOW11:3;
hence  contradiction by A11, A13; ::_thesis: verum
end;
A14: now__::_thesis:_not_z9_=_3_\_2
A15: 1 in 2 by CARD_1:50, TARSKI:def_2;
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
hence  contradiction by A8, A15, TARSKI:def_1, YELLOW11:4; ::_thesis: verum
end;
 ( z9 <> 1 & z9 <> 0 ) by A8, NAT_1:39;
hence  t <= z9 by A4, A9, A12, A14, ENUMSET1:def_4; ::_thesis: verum
end;
A16: for d being Element of B_6 st a >= d & b >= d holds
d <= z
proof
let z9 be Element of B_6; ::_thesis: ( a >= z9 & b >= z9 implies z9 <= z )
assume that
A17: a >= z9 and
A18: b >= z9 ; ::_thesis: z9 <= z
A19: z9 c= 3 \ 1 by A1, A17, YELLOW_1:3;
A20: now__::_thesis:_not_z9_=_1
assume  z9 = 1 ; ::_thesis: contradiction
then  0 in z9 by CARD_1:49, TARSKI:def_1;
hence  contradiction by A19, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
A21: z9 c= 2 by A2, A18, YELLOW_1:3;
A22: now__::_thesis:_not_z9_=_3_\_1
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
then A23: 2 in z9 by TARSKI:def_2, YELLOW11:3;
 not 2 in 2 ;
hence  contradiction by A21, A23; ::_thesis: verum
end;
A24: now__::_thesis:_not_z9_=_3
assume  z9 = 3 ; ::_thesis: contradiction
then A25: 2 in z9 by CARD_1:51, ENUMSET1:def_1;
 not 2 in 2 ;
hence  contradiction by A21, A25; ::_thesis: verum
end;
A26: now__::_thesis:_not_z9_=_3_\_2
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
then A27: 2 in z9 by TARSKI:def_1, YELLOW11:4;
 not 2 in 2 ;
hence  contradiction by A21, A27; ::_thesis: verum
end;
now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then  0 in z9 by CARD_1:50, TARSKI:def_2;
hence  contradiction by A19, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
hence  z9 <= z by A4, A22, A26, A20, A24, ENUMSET1:def_4; ::_thesis: verum
end;
 z c= b by XBOOLE_1:2;
then A28: z <= b by YELLOW_1:3;
 z c= a by XBOOLE_1:2;
then A29: z <= a by YELLOW_1:3;
 a <= t by A1, YELLOW_1:3;
hence  ( a "\/" b = 3 & a "/\" b = 0 ) by A3, A5, A29, A28, A16, YELLOW_0:22, YELLOW_0:23; ::_thesis: verum
end;

theorem Th16: :: ROBBINS4:16
for a, b being Element of B_6 st a = 3 \ 2 & b = 1 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof
 ( 3 in {0,1,(3 \ 1),2,(3 \ 2),3} & 0 in {0,1,(3 \ 1),2,(3 \ 2),3} ) by ENUMSET1:def_4;
then reconsider t = 3, z = 0 as Element of B_6 by YELLOW_1:1;
let a, b be Element of B_6; ::_thesis: ( a = 3 \ 2 & b = 1 implies ( a "\/" b = 3 & a "/\" b = 0 ) )
assume that
A1: a = 3 \ 2 and
A2: b = 1 ; ::_thesis: ( a "\/" b = 3 & a "/\" b = 0 )
 b c= t by A2, NAT_1:39;
then A3: b <= t by YELLOW_1:3;
A4: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A5: for d being Element of B_6 st d >= a & d >= b holds
t <= d
proof
let z9 be Element of B_6; ::_thesis: ( z9 >= a & z9 >= b implies t <= z9 )
assume that
A6: z9 >= a and
A7: z9 >= b ; ::_thesis: t <= z9
A8: 3 \ 2 c= z9 by A1, A6, YELLOW_1:3;
A9: now__::_thesis:_not_z9_=_1
A10: 2 in 3 \ 2 by TARSKI:def_1, YELLOW11:4;
assume  z9 = 1 ; ::_thesis: contradiction
hence  contradiction by A8, A10, CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
A11: now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then A12: not 2 in z9 ;
 2 in 3 \ 2 by TARSKI:def_1, YELLOW11:4;
hence  contradiction by A8, A12; ::_thesis: verum
end;
A13: 1 c= z9 by A2, A7, YELLOW_1:3;
A14: now__::_thesis:_not_z9_=_3_\_2
A15: 0 in 1 by CARD_1:49, TARSKI:def_1;
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
hence  contradiction by A13, A15, TARSKI:def_1, YELLOW11:4; ::_thesis: verum
end;
A16: now__::_thesis:_not_z9_=_3_\_1
A17: 0 in 1 by CARD_1:49, TARSKI:def_1;
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
hence  contradiction by A13, A17, TARSKI:def_2, YELLOW11:3; ::_thesis: verum
end;
 z9 <> 0 by A13;
hence  t <= z9 by A4, A14, A11, A16, A9, ENUMSET1:def_4; ::_thesis: verum
end;
A18: for d being Element of B_6 st a >= d & b >= d holds
d <= z
proof
let z9 be Element of B_6; ::_thesis: ( a >= z9 & b >= z9 implies z9 <= z )
assume that
A19: a >= z9 and
A20: b >= z9 ; ::_thesis: z9 <= z
A21: z9 c= 3 \ 2 by A1, A19, YELLOW_1:3;
A22: now__::_thesis:_not_z9_=_1
assume  z9 = 1 ; ::_thesis: contradiction
then  0 in z9 by CARD_1:49, TARSKI:def_1;
hence  contradiction by A21, TARSKI:def_1, YELLOW11:4; ::_thesis: verum
end;
A23: z9 c= 1 by A2, A20, YELLOW_1:3;
A24: now__::_thesis:_not_z9_=_3_\_2
assume  z9 = 3 \ 2 ; ::_thesis: contradiction
then  2 in z9 by TARSKI:def_1, YELLOW11:4;
hence  contradiction by A23, CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
A25: now__::_thesis:_not_z9_=_3_\_1
assume  z9 = 3 \ 1 ; ::_thesis: contradiction
then A26: 2 in z9 by TARSKI:def_2, YELLOW11:3;
 not 2 in 1 by CARD_1:50, TARSKI:def_2;
hence  contradiction by A23, A26; ::_thesis: verum
end;
A27: now__::_thesis:_not_z9_=_3
assume  z9 = 3 ; ::_thesis: contradiction
then  2 in z9 by CARD_1:51, ENUMSET1:def_1;
hence  contradiction by A23, CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_not_z9_=_2
assume  z9 = 2 ; ::_thesis: contradiction
then  0 in z9 by CARD_1:50, TARSKI:def_2;
hence  contradiction by A21, TARSKI:def_1, YELLOW11:4; ::_thesis: verum
end;
hence  z9 <= z by A4, A25, A24, A22, A27, ENUMSET1:def_4; ::_thesis: verum
end;
 z c= b by XBOOLE_1:2;
then A28: z <= b by YELLOW_1:3;
 z c= a by XBOOLE_1:2;
then A29: z <= a by YELLOW_1:3;
 a <= t by A1, YELLOW_1:3;
hence  ( a "\/" b = 3 & a "/\" b = 0 ) by A3, A5, A29, A28, A18, YELLOW_0:22, YELLOW_0:23; ::_thesis: verum
end;

theorem Th17: :: ROBBINS4:17
for a, b being Element of B_6 st a = 3 \ 1 & b = 1 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof
A1: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
then reconsider z = 3 as Element of B_6 by ENUMSET1:def_4;
A2: 1 c= 3 by NAT_1:39;
let x, y be Element of B_6; ::_thesis: ( x = 3 \ 1 & y = 1 implies ( x "\/" y = 3 & x "/\" y = 0 ) )
assume that
A3: x = 3 \ 1 and
A4: y = 1 ; ::_thesis: ( x "\/" y = 3 & x "/\" y = 0 )
A5: 1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by A2, XBOOLE_1:12 ;
now__::_thesis:_(_x_<=_z_&_y_<=_z_&_(_for_w_being_Element_of_B_6_st_x_<=_w_&_y_<=_w_holds_
z_<=_w_)_)
 y c= z by A4, NAT_1:39;
hence  ( x <= z & y <= z ) by A3, YELLOW_1:3; ::_thesis: for w being Element of B_6 st x <= w & y <= w holds
z <= w
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by A3, A4, A5, YELLOW_1:3; ::_thesis: verum
end;
hence  x "\/" y = 3 by YELLOW_0:22; ::_thesis: x "/\" y = 0
reconsider z = 0 as Element of B_6 by A1, ENUMSET1:def_4;
 x misses y by A3, A4, XBOOLE_1:79;
then A6: x /\ y = 0 by XBOOLE_0:def_7;
now__::_thesis:_(_z_<=_x_&_z_<=_y_&_(_for_w_being_Element_of_B_6_st_w_<=_x_&_w_<=_y_holds_
w_<=_z_)_)
 ( z c= x & z c= y ) by XBOOLE_1:2;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for w being Element of B_6 st w <= x & w <= y holds
w <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by A6; ::_thesis: verum
end;
hence  x "/\" y = 0 by YELLOW_0:23; ::_thesis: verum
end;

theorem Th18: :: ROBBINS4:18
for a, b being Element of B_6 st a = 3 \ 2 & b = 2 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof
A1: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
then reconsider z = 3 as Element of B_6 by ENUMSET1:def_4;
A2: 2 c= 3 by NAT_1:39;
let x, y be Element of B_6; ::_thesis: ( x = 3 \ 2 & y = 2 implies ( x "\/" y = 3 & x "/\" y = 0 ) )
assume that
A3: x = 3 \ 2 and
A4: y = 2 ; ::_thesis: ( x "\/" y = 3 & x "/\" y = 0 )
A5: 2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A2, XBOOLE_1:12 ;
now__::_thesis:_(_x_<=_z_&_y_<=_z_&_(_for_w_being_Element_of_B_6_st_x_<=_w_&_y_<=_w_holds_
z_<=_w_)_)
 y c= z by A4, NAT_1:39;
hence  ( x <= z & y <= z ) by A3, YELLOW_1:3; ::_thesis: for w being Element of B_6 st x <= w & y <= w holds
z <= w
let w be Element of B_6; ::_thesis: ( x <= w & y <= w implies z <= w )
assume  ( x <= w & y <= w ) ; ::_thesis: z <= w
then  ( x c= w & y c= w ) by YELLOW_1:3;
then  x \/ y c= w by XBOOLE_1:8;
hence  z <= w by A3, A4, A5, YELLOW_1:3; ::_thesis: verum
end;
hence  x "\/" y = 3 by YELLOW_0:22; ::_thesis: x "/\" y = 0
reconsider z = 0 as Element of B_6 by A1, ENUMSET1:def_4;
 x misses y by A3, A4, XBOOLE_1:79;
then A6: x /\ y = 0 by XBOOLE_0:def_7;
now__::_thesis:_(_z_<=_x_&_z_<=_y_&_(_for_w_being_Element_of_B_6_st_w_<=_x_&_w_<=_y_holds_
w_<=_z_)_)
 ( z c= x & z c= y ) by XBOOLE_1:2;
hence  ( z <= x & z <= y ) by YELLOW_1:3; ::_thesis: for w being Element of B_6 st w <= x & w <= y holds
w <= z
let w be Element of B_6; ::_thesis: ( w <= x & w <= y implies w <= z )
assume  ( w <= x & w <= y ) ; ::_thesis: w <= z
then  ( w c= x & w c= y ) by YELLOW_1:3;
then  w c= x /\ y by XBOOLE_1:19;
hence  w <= z by A6; ::_thesis: verum
end;
hence  x "/\" y = 0 by YELLOW_0:23; ::_thesis: verum
end;

theorem Th19: :: ROBBINS4:19
for a, b being Element of Benzene st a = 3 \ 1 & b = 2 holds
( a "\/" b = 3 & a "/\" b = 0 )
proof
let a, b be Element of Benzene; ::_thesis: ( a = 3 \ 1 & b = 2 implies ( a "\/" b = 3 & a "/\" b = 0 ) )
assume A1: ( a = 3 \ 1 & b = 2 ) ; ::_thesis: ( a "\/" b = 3 & a "/\" b = 0 )
then  ( a in {0,1,(3 \ 1),2,(3 \ 2),3} & b in {0,1,(3 \ 1),2,(3 \ 2),3} ) by ENUMSET1:def_4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
 ( aa "\/" bb = 3 & aa "/\" bb = 0 ) by A1, Th15;
hence  ( a "\/" b = 3 & a "/\" b = 0 ) by Th14; ::_thesis: verum
end;

theorem :: ROBBINS4:20
for a, b being Element of Benzene st a = 3 \ 2 & b = 1 holds
a "\/" b = 3
proof
let a, b be Element of Benzene; ::_thesis: ( a = 3 \ 2 & b = 1 implies a "\/" b = 3 )
assume A1: ( a = 3 \ 2 & b = 1 ) ; ::_thesis: a "\/" b = 3
then  ( a in {0,1,(3 \ 1),2,(3 \ 2),3} & b in {0,1,(3 \ 1),2,(3 \ 2),3} ) by ENUMSET1:def_4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
 aa "\/" bb = 3 by A1, Th16;
hence  a "\/" b = 3 by Th14; ::_thesis: verum
end;

theorem Th21: :: ROBBINS4:21
for a, b being Element of Benzene st a = 3 \ 1 & b = 1 holds
a "\/" b = 3
proof
let a, b be Element of Benzene; ::_thesis: ( a = 3 \ 1 & b = 1 implies a "\/" b = 3 )
assume A1: ( a = 3 \ 1 & b = 1 ) ; ::_thesis: a "\/" b = 3
then  ( a in {0,1,(3 \ 1),2,(3 \ 2),3} & b in {0,1,(3 \ 1),2,(3 \ 2),3} ) by ENUMSET1:def_4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
 aa "\/" bb = 3 by A1, Th17;
hence  a "\/" b = 3 by Th14; ::_thesis: verum
end;

theorem Th22: :: ROBBINS4:22
for a, b being Element of Benzene st a = 3 \ 2 & b = 2 holds
a "\/" b = 3
proof
let a, b be Element of Benzene; ::_thesis: ( a = 3 \ 2 & b = 2 implies a "\/" b = 3 )
assume A1: ( a = 3 \ 2 & b = 2 ) ; ::_thesis: a "\/" b = 3
then  ( a in {0,1,(3 \ 1),2,(3 \ 2),3} & b in {0,1,(3 \ 1),2,(3 \ 2),3} ) by ENUMSET1:def_4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
 aa "\/" bb = 3 by A1, Th18;
hence  a "\/" b = 3 by Th14; ::_thesis: verum
end;

theorem Th23: :: ROBBINS4:23
for a being Element of Benzene holds
( ( a = 0 implies a ` = 3 ) & ( a = 3 implies a ` = 0 ) & ( a = 1 implies a ` = 3 \ 1 ) & ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
proof
set B = Benzene ;
let a be Element of Benzene; ::_thesis: ( ( a = 0 implies a ` = 3 ) & ( a = 3 implies a ` = 0 ) & ( a = 1 implies a ` = 3 \ 1 ) & ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
 a in the carrier of Benzene ;
then reconsider c = a as Subset of 3 by Th10;
A1: a ` c= c ` by Def4;
A2: a ` = c ` by Def4;
hence  ( a = 0 implies a ` = 3 ) ; ::_thesis: ( ( a = 3 implies a ` = 0 ) & ( a = 1 implies a ` = 3 \ 1 ) & ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
A3: ( a ` = {} or a ` = {0} or a ` = {1} or a ` = {2} or a ` = {0,1} or a ` = {1,2} or a ` = {0,2} or a ` = {0,1,2} ) by A2, YELLOW11:1, ZFMISC_1:118;
thus  ( a = 3 implies a ` = 0 ) ::_thesis: ( ( a = 1 implies a ` = 3 \ 1 ) & ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
proof
assume A4: a = 3 ; ::_thesis: a ` = 0
then  1 in c by ENUMSET1:def_1, YELLOW11:1;
then A5: not 1 in a ` by A1, XBOOLE_0:def_5;
 2 in c by A4, ENUMSET1:def_1, YELLOW11:1;
then A6: not 2 in a ` by A1, XBOOLE_0:def_5;
 not 0 in c ` by A4, XBOOLE_0:def_5;
then  not 0 in a ` by Def4;
hence  a ` = 0 by A3, A5, A6, ENUMSET1:def_1, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum
end;
thus  ( a = 1 implies a ` = 3 \ 1 ) by A2; ::_thesis: ( ( a = 3 \ 1 implies a ` = 1 ) & ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
A7: 0 in 3 by ENUMSET1:def_1, YELLOW11:1;
thus  ( a = 3 \ 1 implies a ` = 1 ) ::_thesis: ( ( a = 2 implies a ` = 3 \ 2 ) & ( a = 3 \ 2 implies a ` = 2 ) )
proof
assume A8: a = 3 \ 1 ; ::_thesis: a ` = 1
then  1 in c by TARSKI:def_2, YELLOW11:3;
then A9: not 1 in a ` by A1, XBOOLE_0:def_5;
 2 in c by A8, TARSKI:def_2, YELLOW11:3;
then A10: not 2 in a ` by A1, XBOOLE_0:def_5;
 not 0 in c by A8, TARSKI:def_2, YELLOW11:3;
hence  a ` = 1 by A7, A2, A3, A9, A10, CARD_1:49, ENUMSET1:def_1, TARSKI:def_1, TARSKI:def_2, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  ( a = 2 implies a ` = 3 \ 2 ) by A2; ::_thesis: ( a = 3 \ 2 implies a ` = 2 )
assume A11: a = 3 \ 2 ; ::_thesis: a ` = 2
then  2 in c by TARSKI:def_1, YELLOW11:4;
then A12: not 2 in a ` by A1, XBOOLE_0:def_5;
 ( 1 in 3 & not 1 in c ) by A11, ENUMSET1:def_1, TARSKI:def_1, YELLOW11:1, YELLOW11:4;
then A13: 1 in a ` by A2, XBOOLE_0:def_5;
 not 0 in c by A11, TARSKI:def_1, YELLOW11:4;
then  0 in a ` by A7, A2, XBOOLE_0:def_5;
hence  a ` = 2 by A3, A12, A13, CARD_1:50, ENUMSET1:def_1, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum
end;

theorem Th24: :: ROBBINS4:24
for a, b being Element of Benzene holds
( a [= b iff a c= b )
proof
let a, b be Element of Benzene; ::_thesis: ( a [= b iff a c= b )
reconsider x = a, y = b as Element of B_6 by Th9, YELLOW_1:1;
hereby  ::_thesis: ( a c= b implies a [= b )
assume  a [= b ; ::_thesis: a c= b
then  x <= y by Th13;
hence  a c= b by YELLOW_1:3; ::_thesis: verum
end;
assume  a c= b ; ::_thesis: a [= b
then  x <= y by YELLOW_1:3;
hence  a [= b by Th13; ::_thesis: verum
end;

theorem Th25: :: ROBBINS4:25
for a, x being Element of Benzene st a = 0 holds
a "/\" x = a
proof
let a, x be Element of Benzene; ::_thesis: ( a = 0 implies a "/\" x = a )
assume  a = 0 ; ::_thesis: a "/\" x = a
then  a c= x by XBOOLE_1:2;
then  a [= x by Th24;
hence  a "/\" x = a by LATTICES:4; ::_thesis: verum
end;

theorem Th26: :: ROBBINS4:26
for a, x being Element of Benzene st a = 0 holds
a "\/" x = x
proof
let a, x be Element of Benzene; ::_thesis: ( a = 0 implies a "\/" x = x )
assume  a = 0 ; ::_thesis: a "\/" x = x
then  a c= x by XBOOLE_1:2;
then  a [= x by Th24;
hence  a "\/" x = x by LATTICES:def_3; ::_thesis: verum
end;

theorem Th27: :: ROBBINS4:27
for a, x being Element of Benzene st a = 3 holds
a "\/" x = a
proof
let a, x be Element of Benzene; ::_thesis: ( a = 3 implies a "\/" x = a )
assume  a = 3 ; ::_thesis: a "\/" x = a
then  x c= a by Th11, YELLOW11:1;
then  x [= a by Th24;
hence  a "\/" x = a by LATTICES:def_3; ::_thesis: verum
end;

registration
cluster Benzene  ->  lower-bounded strict ;
coherence
 Benzene is lower-bounded
proof
reconsider B = 0 as Element of Benzene by Th9, ENUMSET1:def_4;
take  B ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of Benzene holds
( B "/\" b1 = B & b1 "/\" B = B )
 for a being Element of Benzene holds
( B "/\" a = B & a "/\" B = B ) by Th25;
hence  for b1 being Element of the carrier of Benzene holds
( B "/\" b1 = B & b1 "/\" B = B ) ; ::_thesis: verum
end;
cluster Benzene  ->  upper-bounded strict ;
coherence
 Benzene is upper-bounded
proof
reconsider B = 3 as Element of Benzene by Th9, ENUMSET1:def_4;
take  B ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of Benzene holds
( B "\/" b1 = B & b1 "\/" B = B )
 for a being Element of Benzene holds
( B "\/" a = B & a "\/" B = B ) by Th27;
hence  for b1 being Element of the carrier of Benzene holds
( B "\/" b1 = B & b1 "\/" B = B ) ; ::_thesis: verum
end;
end;

theorem :: ROBBINS4:28
Top Benzene = 3
proof
reconsider x = 3 as Element of Benzene by Th9, ENUMSET1:def_4;
 for a being Element of Benzene holds
( x "\/" a = x & a "\/" x = x ) by Th27;
hence  Top Benzene = 3 by LATTICES:def_17; ::_thesis: verum
end;

theorem Th29: :: ROBBINS4:29
Bottom Benzene = 0
proof
reconsider x = 0 as Element of Benzene by Th9, ENUMSET1:def_4;
 for a being Element of Benzene holds
( x "/\" a = x & a "/\" x = x ) by Th25;
hence  Bottom Benzene = 0 by LATTICES:def_16; ::_thesis: verum
end;

registration
cluster Benzene  ->  strict de_Morgan involutive with_Top ;
coherence
 ( Benzene is involutive & Benzene is with_Top & Benzene is de_Morgan )
proof
set B = Benzene ;
 for a being Element of Benzene holds (a `) ` = a
proof
let a be Element of Benzene; ::_thesis: (a `) ` = a
percases ( a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 ) by Th9, ENUMSET1:def_4;
supposeA1: a = 0 ; ::_thesis: (a `) ` = a
then  a ` = 3 by Th23;
hence  (a `) ` = a by A1, Th23; ::_thesis: verum
end;
supposeA2: a = 1 ; ::_thesis: (a `) ` = a
then  a ` = 3 \ 1 by Th23;
hence  (a `) ` = a by A2, Th23; ::_thesis: verum
end;
supposeA3: a = 3 \ 1 ; ::_thesis: (a `) ` = a
then  a ` = 1 by Th23;
hence  (a `) ` = a by A3, Th23; ::_thesis: verum
end;
supposeA4: a = 2 ; ::_thesis: (a `) ` = a
then  a ` = 3 \ 2 by Th23;
hence  (a `) ` = a by A4, Th23; ::_thesis: verum
end;
supposeA5: a = 3 \ 2 ; ::_thesis: (a `) ` = a
then  a ` = 2 by Th23;
hence  (a `) ` = a by A5, Th23; ::_thesis: verum
end;
supposeA6: a = 3 ; ::_thesis: (a `) ` = a
then  a ` = 0 by Th23;
hence  (a `) ` = a by A6, Th23; ::_thesis: verum
end;
end;
end;
hence A7: Benzene is involutive by ROBBINS3:def_6; ::_thesis: ( Benzene is with_Top & Benzene is de_Morgan )
A8: for a being Element of Benzene holds a "\/" (a `) = 3
proof
let a be Element of Benzene; ::_thesis: a "\/" (a `) = 3
percases ( a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 ) by Th9, ENUMSET1:def_4;
supposeA9: a = 0 ; ::_thesis: a "\/" (a `) = 3
then  a ` = 3 by Th23;
hence  a "\/" (a `) = 3 by A9, Th26; ::_thesis: verum
end;
supposeA10: a = 1 ; ::_thesis: a "\/" (a `) = 3
then  a ` = 3 \ 1 by Th23;
hence  a "\/" (a `) = 3 by A10, Th21; ::_thesis: verum
end;
supposeA11: a = 3 \ 1 ; ::_thesis: a "\/" (a `) = 3
then  a ` = 1 by Th23;
hence  a "\/" (a `) = 3 by A11, Th21; ::_thesis: verum
end;
supposeA12: a = 2 ; ::_thesis: a "\/" (a `) = 3
then  a ` = 3 \ 2 by Th23;
hence  a "\/" (a `) = 3 by A12, Th22; ::_thesis: verum
end;
supposeA13: a = 3 \ 2 ; ::_thesis: a "\/" (a `) = 3
then  a ` = 2 by Th23;
hence  a "\/" (a `) = 3 by A13, Th22; ::_thesis: verum
end;
suppose a = 3 ; ::_thesis: a "\/" (a `) = 3
hence  a "\/" (a `) = 3 by Th27; ::_thesis: verum
end;
end;
end;
thus  Benzene is with_Top ::_thesis: Benzene is de_Morgan
proof
let a, b be Element of Benzene; :: according to ROBBINS3:def_7 ::_thesis: a "\/" (a `) = b "\/" (b `)
 a "\/" (a `) = 3 by A8;
hence  a "\/" (a `) = b "\/" (b `) by A8; ::_thesis: verum
end;
 for a, b being Element of Benzene st a [= b holds
b ` [= a `
proof
let a, b be Element of Benzene; ::_thesis: ( a [= b implies b ` [= a ` )
reconsider x = a, y = b as Subset of {0,1,2} by Th11;
reconsider x = x, y = y as Subset of 3 by CARD_1:51;
assume  a [= b ; ::_thesis: b ` [= a `
then  x c= y by Th24;
then A14: y ` c= x ` by SUBSET_1:12;
 ( a ` = x ` & b ` = y ` ) by Def4;
hence  b ` [= a ` by A14, Th24; ::_thesis: verum
end;
hence  Benzene is de_Morgan by A7, Th4; ::_thesis: verum
end;
cluster Benzene  ->  strict non orthomodular ;
coherence
 not Benzene is orthomodular
proof
 ex x, y being Element of Benzene st
( x [= y & not y = x "\/" ((x `) "/\" y) )
proof
set y = 2;
set x = 1;
reconsider x = 1, y = 2 as Element of Benzene by Th9, ENUMSET1:def_4;
 for z being set st z in 1 holds
z in 2
proof
let z be set ; ::_thesis: ( z in 1 implies z in 2 )
assume  z in 1 ; ::_thesis: z in 2
then  z = 0 by CARD_1:49, TARSKI:def_1;
hence  z in 2 by CARD_1:50, TARSKI:def_2; ::_thesis: verum
end;
then  1 c= 2 by TARSKI:def_3;
then A15: x [= y by Th24;
 x ` = 3 \ 1 by Th23;
then  (x `) "/\" y = 0 by Th19;
then  x "\/" ((x `) "/\" y) = x by Th29, LATTICES:14;
hence  ex x, y being Element of Benzene st
( x [= y & not y = x "\/" ((x `) "/\" y) ) by A15; ::_thesis: verum
end;
hence  not Benzene is orthomodular by Def1; ::_thesis: verum
end;
end;

begin

definition
let L be Ortholattice;
let a, b be Element of L;
preda,b are_orthogonal  means :Def5: :: ROBBINS4:def 5
a [= b ` ;
end;

:: deftheorem Def5 defines are_orthogonal ROBBINS4:def_5_:_
 for L being Ortholattice
for a, b being Element of L holds
( a,b are_orthogonal iff a [= b ` );

notation
let L be Ortholattice;
let a, b be Element of L;
synonym a _|_ b for a,b are_orthogonal ;
end;

theorem :: ROBBINS4:30
for L being Ortholattice
for a being Element of L holds
( a _|_ a iff a = Bottom L )
proof
let L be Ortholattice; ::_thesis: for a being Element of L holds
( a _|_ a iff a = Bottom L )
let a be Element of L; ::_thesis: ( a _|_ a iff a = Bottom L )
thus  ( a _|_ a implies a = Bottom L ) ::_thesis: ( a = Bottom L implies a _|_ a )
proof
assume  a _|_ a ; ::_thesis: a = Bottom L
then  a [= a ` by Def5;
then  a "/\" (a `) = a by LATTICES:4;
hence  a = Bottom L by Th2; ::_thesis: verum
end;
assume  a = Bottom L ; ::_thesis: a _|_ a
then  a "/\" (a `) = a by Th2;
then  a [= a ` by LATTICES:4;
hence  a _|_ a by Def5; ::_thesis: verum
end;

definition
let L be Ortholattice;
let a, b be Element of L;
:: original: are_orthogonal
redefine preda,b are_orthogonal ;
symmetry
 for a, b being Element of L st (L,b1,b2) holds
(L,b2,b1)
proof
let a, b be Element of L; ::_thesis: ( (L,a,b) implies (L,b,a) )
assume  a _|_ b ; ::_thesis: (L,b,a)
then  a [= b ` by Def5;
then  (b `) ` [= a ` by Th4;
then  b [= a ` by ROBBINS3:def_6;
hence  (L,b,a) by Def5; ::_thesis: verum
end;
end;

theorem :: ROBBINS4:31
for L being Ortholattice
for a, b, c being Element of L st a _|_ b & a _|_ c holds
( a _|_ b "/\" c & a _|_ b "\/" c )
proof
let L be Ortholattice; ::_thesis: for a, b, c being Element of L st a _|_ b & a _|_ c holds
( a _|_ b "/\" c & a _|_ b "\/" c )
let a, b, c be Element of L; ::_thesis: ( a _|_ b & a _|_ c implies ( a _|_ b "/\" c & a _|_ b "\/" c ) )
assume  a _|_ b ; ::_thesis: ( not a _|_ c or ( a _|_ b "/\" c & a _|_ b "\/" c ) )
then A1: a [= b ` by Def5;
then A2: a "/\" (c `) [= (b `) "/\" (c `) by LATTICES:9;
assume A3: a _|_ c ; ::_thesis: ( a _|_ b "/\" c & a _|_ b "\/" c )
 b ` [= (b `) "\/" (c `) by LATTICES:5;
then  a [= (b `) "\/" (c `) by A1, LATTICES:7;
then  a [= (((b `) "\/" (c `)) `) ` by ROBBINS3:def_6;
then  a [= (b "/\" c) ` by ROBBINS1:def_23;
hence  a _|_ b "/\" c by Def5; ::_thesis: a _|_ b "\/" c
 a [= c ` by A3, Def5;
then  a [= (b `) "/\" (c `) by A2, LATTICES:4;
then  a [= (((b `) `) "\/" ((c `) `)) ` by ROBBINS1:def_23;
then  a [= (b "\/" ((c `) `)) ` by ROBBINS3:def_6;
then  a [= (b "\/" c) ` by ROBBINS3:def_6;
hence  a _|_ b "\/" c by Def5; ::_thesis: verum
end;

begin

theorem :: ROBBINS4:32
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
a = b ` )
proof
let L be Ortholattice; ::_thesis: ( L is orthomodular iff for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
a = b ` )
thus  ( L is orthomodular implies for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
a = b ` ) ::_thesis: ( ( for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
a = b ` ) implies L is orthomodular )
proof
assume A1: L is orthomodular ; ::_thesis: for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
a = b `
let x, y be Element of L; ::_thesis: ( y ` [= x & x "/\" y = Bottom L implies x = y ` )
assume A2: y ` [= x ; ::_thesis: ( not x "/\" y = Bottom L or x = y ` )
assume A3: x "/\" y = Bottom L ; ::_thesis: x = y `
thus x = (y `) "\/" (((y `) `) "/\" x) by A1, A2, Def1
.= (y `) "\/" (y "/\" x) by ROBBINS3:def_6
.= y ` by A3, LATTICES:14 ; ::_thesis: verum
end;
assume A4: for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
a = b ` ; ::_thesis: L is orthomodular
let x, y be Element of L; :: according to ROBBINS4:def_1 ::_thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )
assume  x [= y ; ::_thesis: y = x "\/" ((x `) "/\" y)
then  x "\/" ((x `) "/\" y) [= y "\/" ((x `) "/\" y) by FILTER_0:1;
then  x "\/" ((x `) "/\" y) [= y by LATTICES:def_8;
then A5: ((x "\/" ((x `) "/\" y)) `) ` [= y by ROBBINS3:def_6;
((x "\/" ((x `) "/\" y)) `) "/\" y = y "/\" ((((x `) `) "\/" ((x `) "/\" y)) `) by ROBBINS3:def_6
.= y "/\" ((((x `) `) "\/" ((((x `) "/\" y) `) `)) `) by ROBBINS3:def_6
.= y "/\" ((x `) "/\" (((x `) "/\" y) `)) by ROBBINS1:def_23
.= y "/\" ((x `) "/\" (((((x `) `) "\/" (y `)) `) `)) by ROBBINS1:def_23
.= y "/\" ((x `) "/\" (((x `) `) "\/" (y `))) by ROBBINS3:def_6
.= y "/\" ((x `) "/\" (x "\/" (y `))) by ROBBINS3:def_6
.= (y "/\" (x `)) "/\" (x "\/" (y `)) by LATTICES:def_7
.= (((y `) "\/" ((x `) `)) `) "/\" (x "\/" (y `)) by ROBBINS1:def_23
.= ((x "\/" (y `)) `) "/\" (x "\/" (y `)) by ROBBINS3:def_6
.= Bottom L by Th2 ;
then  ((x "\/" ((x `) "/\" y)) `) ` = y by A4, A5;
hence  y = x "\/" ((x `) "/\" y) by ROBBINS3:def_6; ::_thesis: verum
end;

theorem :: ROBBINS4:33
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
a = b ` )
proof
let L be Ortholattice; ::_thesis: ( L is orthomodular iff for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
a = b ` )
thus  ( L is orthomodular implies for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
a = b ` ) ::_thesis: ( ( for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
a = b ` ) implies L is orthomodular )
proof
assume A1: L is orthomodular ; ::_thesis: for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
a = b `
let x, y be Element of L; ::_thesis: ( x _|_ y & x "\/" y = Top L implies x = y ` )
assume  x _|_ y ; ::_thesis: ( not x "\/" y = Top L or x = y ` )
then A2: x [= y ` by Def5;
assume A3: x "\/" y = Top L ; ::_thesis: x = y `
thus y ` = x "\/" ((x `) "/\" (y `)) by A1, A2, Def1
.= x "\/" ((((x `) `) "\/" ((y `) `)) `) by ROBBINS1:def_23
.= x "\/" ((x "\/" ((y `) `)) `) by ROBBINS3:def_6
.= x "\/" ((x "\/" y) `) by ROBBINS3:def_6
.= x "\/" ((((x `) `) "\/" (x `)) `) by A3, Th2
.= x "\/" ((x `) "/\" x) by ROBBINS1:def_23
.= x by LATTICES:def_8 ; ::_thesis: verum
end;
assume A4: for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
a = b ` ; ::_thesis: L is orthomodular
let x, y be Element of L; :: according to ROBBINS4:def_1 ::_thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )
assume  x [= y ; ::_thesis: y = x "\/" ((x `) "/\" y)
then  x "\/" ((x `) "/\" y) [= y "\/" ((x `) "/\" y) by FILTER_0:1;
then  x "\/" ((x `) "/\" y) [= y by LATTICES:def_8;
then  x "\/" ((x `) "/\" y) [= (y `) ` by ROBBINS3:def_6;
then A5: x "\/" ((x `) "/\" y) _|_ y ` by Def5;
(y `) "\/" (x "\/" ((x `) "/\" y)) = ((y `) "\/" x) "\/" ((x `) "/\" y) by LATTICES:def_5
.= ((y `) "\/" ((x `) `)) "\/" ((x `) "/\" y) by ROBBINS3:def_6
.= ((((y `) "\/" ((x `) `)) `) `) "\/" ((x `) "/\" y) by ROBBINS3:def_6
.= ((y "/\" (x `)) `) "\/" ((x `) "/\" y) by ROBBINS1:def_23
.= Top L by Th2 ;
then  x "\/" ((x `) "/\" y) = (y `) ` by A4, A5;
hence  y = x "\/" ((x `) "/\" y) by ROBBINS3:def_6; ::_thesis: verum
end;

theorem Th34: :: ROBBINS4:34
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st b [= a holds
a "/\" ((a `) "\/" b) = b )
proof
let L be Ortholattice; ::_thesis: ( L is orthomodular iff for a, b being Element of L st b [= a holds
a "/\" ((a `) "\/" b) = b )
thus  ( L is orthomodular implies for a, b being Element of L st b [= a holds
a "/\" ((a `) "\/" b) = b ) ::_thesis: ( ( for a, b being Element of L st b [= a holds
a "/\" ((a `) "\/" b) = b ) implies L is orthomodular )
proof
assume A1: L is orthomodular ; ::_thesis: for a, b being Element of L st b [= a holds
a "/\" ((a `) "\/" b) = b
let a, b be Element of L; ::_thesis: ( b [= a implies a "/\" ((a `) "\/" b) = b )
assume  b [= a ; ::_thesis: a "/\" ((a `) "\/" b) = b
then  a ` [= b ` by Th4;
then b ` = (a `) "\/" (((a `) `) "/\" (b `)) by A1, Def1
.= (a `) "\/" (a "/\" (b `)) by ROBBINS3:def_6
.= (a `) "\/" (((a `) "\/" ((b `) `)) `) by ROBBINS1:def_23
.= (a `) "\/" (((a `) "\/" b) `) by ROBBINS3:def_6
.= (((a `) "\/" (((a `) "\/" b) `)) `) ` by ROBBINS3:def_6
.= (a "/\" ((a `) "\/" b)) ` by ROBBINS1:def_23 ;
then  (b `) ` = a "/\" ((a `) "\/" b) by ROBBINS3:def_6;
hence  a "/\" ((a `) "\/" b) = b by ROBBINS3:def_6; ::_thesis: verum
end;
assume A2: for a, b being Element of L st b [= a holds
a "/\" ((a `) "\/" b) = b ; ::_thesis: L is orthomodular
let a, b be Element of L; :: according to ROBBINS4:def_1 ::_thesis: ( a [= b implies b = a "\/" ((a `) "/\" b) )
assume  a [= b ; ::_thesis: b = a "\/" ((a `) "/\" b)
then  b ` [= a ` by Th4;
then b ` = (a `) "/\" (((a `) `) "\/" (b `)) by A2
.= (a `) "/\" (((((a `) `) "\/" (b `)) `) `) by ROBBINS3:def_6
.= (a `) "/\" (((a `) "/\" b) `) by ROBBINS1:def_23
.= (((a `) `) "\/" ((((a `) "/\" b) `) `)) ` by ROBBINS1:def_23
.= (a "\/" ((((a `) "/\" b) `) `)) ` by ROBBINS3:def_6
.= (a "\/" ((a `) "/\" b)) ` by ROBBINS3:def_6 ;
then  (b `) ` = a "\/" ((a `) "/\" b) by ROBBINS3:def_6;
hence  b = a "\/" ((a `) "/\" b) by ROBBINS3:def_6; ::_thesis: verum
end;

theorem :: ROBBINS4:35
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b )
proof
let L be Ortholattice; ::_thesis: ( L is orthomodular iff for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b )
thus  ( L is orthomodular implies for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ) ::_thesis: ( ( for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ) implies L is orthomodular )
proof
assume A1: L is orthomodular ; ::_thesis: for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b
let a, b be Element of L; ::_thesis: a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b
 a "/\" b [= a by LATTICES:6;
hence  a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b by A1, Th34; ::_thesis: verum
end;
assume A2: for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ; ::_thesis: L is orthomodular
 for a, b being Element of L st b [= a holds
a "/\" ((a `) "\/" b) = b
proof
let a, b be Element of L; ::_thesis: ( b [= a implies a "/\" ((a `) "\/" b) = b )
assume A3: b [= a ; ::_thesis: a "/\" ((a `) "\/" b) = b
hence b = a "/\" b by LATTICES:4
.= a "/\" ((a `) "\/" (a "/\" b)) by A2
.= a "/\" ((a `) "\/" b) by A3, LATTICES:4 ;
::_thesis: verum
end;
hence  L is orthomodular by Th34; ::_thesis: verum
end;

theorem Th36: :: ROBBINS4:36
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) )
proof
let L be Ortholattice; ::_thesis: ( L is orthomodular iff for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) )
thus  ( L is orthomodular implies for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) ) ::_thesis: ( ( for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) ) implies L is orthomodular )
proof
assume A1: L is orthomodular ; ::_thesis: for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `))
let a, b be Element of L; ::_thesis: a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `))
 a "\/" b = a "\/" ((a "\/" b) "/\" (a `)) by A1, Th6;
hence  a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) by LATTICES:def_9; ::_thesis: verum
end;
assume A2: for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) ; ::_thesis: L is orthomodular
let x, y be Element of L; :: according to ROBBINS4:def_1 ::_thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )
assume A3: x [= y ; ::_thesis: y = x "\/" ((x `) "/\" y)
hence y = x "\/" y by LATTICES:def_3
.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" (x `)) by A2
.= (y "/\" x) "\/" ((x "\/" y) "/\" (x `)) by A3, LATTICES:def_3
.= (y "/\" x) "\/" (y "/\" (x `)) by A3, LATTICES:def_3
.= x "\/" ((x `) "/\" y) by A3, LATTICES:4 ;
::_thesis: verum
end;

theorem :: ROBBINS4:37
for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) )
proof
let L be Ortholattice; ::_thesis: ( L is orthomodular iff for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) )
thus  ( L is orthomodular implies for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) ) ::_thesis: ( ( for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) ) implies L is orthomodular )
proof
assume A1: L is orthomodular ; ::_thesis: for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `))
let a, b be Element of L; ::_thesis: ( a [= b implies (a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) )
assume A2: a [= b ; ::_thesis: (a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `))
 ( a "/\" b [= a "\/" b & b "/\" (a `) [= a "\/" b ) by FILTER_0:3, LATTICES:6;
then A3: (a "/\" b) "\/" (b "/\" (a `)) [= a "\/" b by FILTER_0:6;
 ( a "/\" b [= b "\/" (a `) & b "/\" (a `) [= b "\/" (a `) ) by FILTER_0:3, LATTICES:6;
then  (a "/\" b) "\/" (b "/\" (a `)) [= b "\/" (a `) by FILTER_0:6;
then A4: (a "/\" b) "\/" (b "/\" (a `)) [= (a "\/" b) "/\" (b "\/" (a `)) by A3, FILTER_0:7;
A5: (a "\/" b) "/\" (b "\/" (a `)) [= a "\/" b by LATTICES:6;
a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) by A1, Th36
.= (b "/\" a) "\/" ((a "\/" b) "/\" (a `)) by A2, LATTICES:def_3
.= (b "/\" a) "\/" (b "/\" (a `)) by A2, LATTICES:def_3 ;
hence  (a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) by A4, A5, LATTICES:8; ::_thesis: verum
end;
assume A6: for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) ; ::_thesis: L is orthomodular
let a be Element of L; :: according to ROBBINS4:def_1 ::_thesis: for y being Element of L st a [= y holds
y = a "\/" ((a `) "/\" y)
let b be Element of L; ::_thesis: ( a [= b implies b = a "\/" ((a `) "/\" b) )
assume A7: a [= b ; ::_thesis: b = a "\/" ((a `) "/\" b)
then (a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) by A6
.= a "\/" ((a `) "/\" b) by A7, LATTICES:4 ;
hence a "\/" ((a `) "/\" b) = b "/\" (b "\/" (a `)) by A7, LATTICES:def_3
.= b by LATTICES:def_9 ;
::_thesis: verum
end;

theorem :: ROBBINS4:38
for L being non empty OrthoLattStr holds
( L is Orthomodular_Lattice iff ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) )
proof
let L be non empty OrthoLattStr ; ::_thesis: ( L is Orthomodular_Lattice iff ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) )
thus  ( L is Orthomodular_Lattice implies ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) ) ::_thesis: ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) implies L is Orthomodular_Lattice )
proof
assume A1: L is Orthomodular_Lattice ; ::_thesis: ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) )
hence  for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a by Th3; ::_thesis: ( ( for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) )
thus  for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) ::_thesis: for a, b being Element of L holds a = a "\/" (b "/\" (b `))
proof
let a, b, c be Element of L; ::_thesis: a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `))
 ( (a "\/" b) "/\" (a `) [= a "\/" b & (a "\/" b) "/\" (a "\/" c) [= a "\/" b ) by A1, LATTICES:6;
then A2: ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) [= a "\/" b by A1, FILTER_0:6;
 a "/\" (a "\/" b) [= (a "\/" c) "/\" (a "\/" b) by A1, LATTICES:5, LATTICES:9;
then  (a "\/" b) "/\" a [= (a "\/" c) "/\" (a "\/" b) by A1, LATTICES:def_6;
then  (a "\/" b) "/\" a [= (a "\/" b) "/\" (a "\/" c) by A1, LATTICES:def_6;
then  ((a "\/" b) "/\" (a `)) "\/" ((a "\/" b) "/\" a) [= ((a "\/" b) "/\" (a `)) "\/" ((a "\/" b) "/\" (a "\/" c)) by A1, FILTER_0:1;
then A3: ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) [= ((a "\/" b) "/\" (a `)) "\/" ((a "\/" b) "/\" (a "\/" c)) by A1, LATTICES:def_4;
 a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) by A1, Th36;
then  a "\/" b [= ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) by A1, A3, LATTICES:def_4;
hence  a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) by A1, A2, LATTICES:8; ::_thesis: verum
end;
thus  for a, b being Element of L holds a = a "\/" (b "/\" (b `)) by A1, Th3; ::_thesis: verum
end;
assume A4: for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ; ::_thesis: ( ex a, b, c being Element of L st not a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) or ex a, b being Element of L st not a = a "\/" (b "/\" (b `)) or L is Orthomodular_Lattice )
assume A5: for a, b, c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a `)) ; ::_thesis: ( ex a, b being Element of L st not a = a "\/" (b "/\" (b `)) or L is Orthomodular_Lattice )
assume A6: for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ; ::_thesis: L is Orthomodular_Lattice
A7: for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `))
proof
let a, b be Element of L; ::_thesis: a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `))
set c = a "/\" (a `);
 a "\/" b = ((a "\/" b) "/\" (a "\/" (a "/\" (a `)))) "\/" ((a "\/" b) "/\" (a `)) by A5;
hence  a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) by A6; ::_thesis: verum
end;
 for a, c being Element of L holds a = a "/\" (a "\/" c)
proof
let a, c be Element of L; ::_thesis: a = a "/\" (a "\/" c)
set b = a "/\" (a `);
thus a = a "\/" (a "/\" (a `)) by A6
.= ((a "\/" (a "/\" (a `))) "/\" (a "\/" c)) "\/" ((a "\/" (a "/\" (a `))) "/\" (a `)) by A5
.= (a "/\" (a "\/" c)) "\/" ((a "\/" (a "/\" (a `))) "/\" (a `)) by A6
.= (a "/\" (a "\/" c)) "\/" (a "/\" (a `)) by A6
.= a "/\" (a "\/" c) by A6 ; ::_thesis: verum
end;
then  L is Ortholattice by A4, A6, Th3;
hence  L is Orthomodular_Lattice by A7, Th36; ::_thesis: verum
end;


registration
cluster non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular  ->  non empty Lattice-like de_Morgan join-Associative meet-Absorbing with_Top orthomodular for OrthoLattStr ;
coherence
 for b1 being non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular OrthoLattStr holds b1 is with_Top
proof
let L be non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular OrthoLattStr ; ::_thesis: L is with_Top
deffunc H1( Element of L) ->  Element of the carrier of L = c1 ` ;
 for x, y being Element of L holds x "\/" H1(x) = y "\/" H1(y)
proof
A1: for v0, v1 being Element of L holds v0 "\/" H1(H1(v0) "\/" H1(v1)) = v0
proof
let v0, v1 be Element of L; ::_thesis: v0 "\/" H1(H1(v0) "\/" H1(v1)) = v0
 v0 "/\" v1 = H1(H1(v0) "\/" H1(v1)) by ROBBINS1:def_23;
hence  v0 "\/" H1(H1(v0) "\/" H1(v1)) = v0 by ROBBINS3:def_3; ::_thesis: verum
end;
A2: for v64 being Element of L holds v64 "\/" H1(H1(v64)) = v64
proof
let v64 be Element of L; ::_thesis: v64 "\/" H1(H1(v64)) = v64
now__::_thesis:_for_v64,_v1_being_Element_of_L_holds_v64_"\/"_H1(H1(v64))_=_v64
let v64, v1 be Element of L; ::_thesis: v64 "\/" H1(H1(v64)) = v64
 H1(v64) "\/" H1(H1(H1(v64)) "\/" H1(v1)) = H1(v64) by A1;
hence  v64 "\/" H1(H1(v64)) = v64 by A1; ::_thesis: verum
end;
hence  v64 "\/" H1(H1(v64)) = v64 ; ::_thesis: verum
end;
A3: for v0, v1 being Element of L holds v0 "\/" H1(H1(H1(v0)) "\/" H1(v0 "\/" v1)) = v0 "\/" v1
proof
let v0, v1 be Element of L; ::_thesis: v0 "\/" H1(H1(H1(v0)) "\/" H1(v0 "\/" v1)) = v0 "\/" v1
 H1(v0) "/\" (v0 "\/" v1) = H1(H1(H1(v0)) "\/" H1(v0 "\/" v1)) by ROBBINS1:def_23;
hence  v0 "\/" H1(H1(H1(v0)) "\/" H1(v0 "\/" v1)) = v0 "\/" v1 by Def2; ::_thesis: verum
end;
A4: for v64, v1 being Element of L holds v64 "\/" H1(H1(v64) "\/" v1) = v64
proof
let v64, v1 be Element of L; ::_thesis: v64 "\/" H1(H1(v64) "\/" v1) = v64
 H1(v64) "\/" H1(H1(H1(H1(v64))) "\/" H1(H1(v64) "\/" v1)) = H1(v64) "\/" v1 by A3;
hence  v64 "\/" H1(H1(v64) "\/" v1) = v64 by A1; ::_thesis: verum
end;
A5: for v64, v65, v1 being Element of L holds v64 "\/" v65 = v65 "\/" (v64 "\/" H1(H1(v65) "\/" v1))
proof
let v64, v65, v1 be Element of L; ::_thesis: v64 "\/" v65 = v65 "\/" (v64 "\/" H1(H1(v65) "\/" v1))
 v65 "\/" H1(H1(v65) "\/" v1) = v65 by A4;
hence  v64 "\/" v65 = v65 "\/" (v64 "\/" H1(H1(v65) "\/" v1)) by ROBBINS3:def_1; ::_thesis: verum
end;
A6: for v64, v65 being Element of L holds v64 "\/" v65 = v65 "\/" (v64 "\/" H1(H1(v65)))
proof
let v64, v65 be Element of L; ::_thesis: v64 "\/" v65 = v65 "\/" (v64 "\/" H1(H1(v65)))
 v65 "\/" H1(H1(v65)) = v65 by A2;
hence  v64 "\/" v65 = v65 "\/" (v64 "\/" H1(H1(v65))) by ROBBINS3:def_1; ::_thesis: verum
end;
A7: for v64 being Element of L holds v64 "\/" ((v64 `) `) = ((((v64 `) `) `) `) "\/" v64
proof
let v64 be Element of L; ::_thesis: v64 "\/" ((v64 `) `) = ((((v64 `) `) `) `) "\/" v64
 ((((v64 `) `) `) `) "\/" ((v64 `) `) = (v64 `) ` by A2;
hence  v64 "\/" ((v64 `) `) = ((((v64 `) `) `) `) "\/" v64 by A6; ::_thesis: verum
end;
A8: for v64 being Element of L holds v64 = ((((v64 `) `) `) `) "\/" v64
proof
let v64 be Element of L; ::_thesis: v64 = ((((v64 `) `) `) `) "\/" v64
 v64 "\/" ((v64 `) `) = v64 by A2;
hence  v64 = ((((v64 `) `) `) `) "\/" v64 by A7; ::_thesis: verum
end;
A9: for v65 being Element of L holds (((v65 `) `) `) "\/" (v65 `) = ((v65 `) `) `
proof
let v65 be Element of L; ::_thesis: (((v65 `) `) `) "\/" (v65 `) = ((v65 `) `) `
 ((((v65 `) `) `) `) "\/" v65 = v65 by A8;
hence  (((v65 `) `) `) "\/" (v65 `) = ((v65 `) `) ` by A4; ::_thesis: verum
end;
A10: for v65 being Element of L holds v65 ` = ((v65 `) `) `
proof
let v65 be Element of L; ::_thesis: v65 ` = ((v65 `) `) `
 (((v65 `) `) `) "\/" (v65 `) = v65 ` by A2;
hence  v65 ` = ((v65 `) `) ` by A9; ::_thesis: verum
end;
A11: for v65 being Element of L holds H1(H1(H1(H1(v65)))) "\/" H1(H1(H1(H1(H1(H1(H1(v65)))))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65
proof
let v65 be Element of L; ::_thesis: H1(H1(H1(H1(v65)))) "\/" H1(H1(H1(H1(H1(H1(H1(v65)))))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65
 H1(H1(H1(H1(v65)))) "\/" v65 = v65 by A8;
hence  H1(H1(H1(H1(v65)))) "\/" H1(H1(H1(H1(H1(H1(H1(v65)))))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65 by A3; ::_thesis: verum
end;
A12: for v65 being Element of L holds H1(H1(v65)) "\/" H1(H1(H1(H1(H1(H1(H1(v65)))))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65
proof
let v65 be Element of L; ::_thesis: H1(H1(v65)) "\/" H1(H1(H1(H1(H1(H1(H1(v65)))))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65
 ((v65 `) `) ` = v65 ` by A10;
hence  H1(H1(v65)) "\/" H1(H1(H1(H1(H1(H1(H1(v65)))))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65 by A11; ::_thesis: verum
end;
A13: for v65 being Element of L holds H1(H1(v65)) "\/" H1(H1(H1(H1(H1(v65)))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65
proof
let v65 be Element of L; ::_thesis: H1(H1(v65)) "\/" H1(H1(H1(H1(H1(v65)))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65
 ((v65 `) `) ` = v65 ` by A10;
hence  H1(H1(v65)) "\/" H1(H1(H1(H1(H1(v65)))) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65 by A12; ::_thesis: verum
end;
A14: for v65 being Element of L holds H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65
proof
let v65 be Element of L; ::_thesis: H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65
 ((v65 `) `) ` = v65 ` by A10;
hence  H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = H1(H1(H1(H1(v65)))) "\/" v65 by A13; ::_thesis: verum
end;
A15: for v65 being Element of L holds H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = H1(H1(v65)) "\/" v65
proof
let v65 be Element of L; ::_thesis: H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = H1(H1(v65)) "\/" v65
 ((v65 `) `) ` = v65 ` by A10;
hence  H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = H1(H1(v65)) "\/" v65 by A14; ::_thesis: verum
end;
A16: for v65 being Element of L holds H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = v65
proof
let v65 be Element of L; ::_thesis: H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = v65
 ((v65 `) `) "\/" v65 = v65 by A2;
hence  H1(H1(v65)) "\/" H1(H1(H1(v65)) "\/" H1(v65)) = v65 by A15; ::_thesis: verum
end;
A17: for v0, v65 being Element of L holds H1(H1(v0)) "\/" H1(v65 "\/" H1(v0)) = (v0 `) `
proof
let v0, v65 be Element of L; ::_thesis: H1(H1(v0)) "\/" H1(v65 "\/" H1(v0)) = (v0 `) `
 ((v0 `) `) ` = v0 ` by A10;
hence  H1(H1(v0)) "\/" H1(v65 "\/" H1(v0)) = (v0 `) ` by A4; ::_thesis: verum
end;
A18: for v0 being Element of L holds (v0 `) ` = v0
proof
let v0 be Element of L; ::_thesis: (v0 `) ` = v0
 H1(H1(v0)) "\/" H1(H1(H1(v0)) "\/" H1(v0)) = (v0 `) ` by A17;
hence  (v0 `) ` = v0 by A16; ::_thesis: verum
end;
A19: for v64, v1 being Element of L holds v64 "\/" H1(H1(H1(v64)) "\/" H1(v1 "\/" v64)) = v64 "\/" (v1 "\/" H1(H1(v64)))
proof
let v64, v1 be Element of L; ::_thesis: v64 "\/" H1(H1(H1(v64)) "\/" H1(v1 "\/" v64)) = v64 "\/" (v1 "\/" H1(H1(v64)))
 v64 "\/" (v1 "\/" H1(H1(v64))) = v1 "\/" v64 by A6;
hence  v64 "\/" H1(H1(H1(v64)) "\/" H1(v1 "\/" v64)) = v64 "\/" (v1 "\/" H1(H1(v64))) by A3; ::_thesis: verum
end;
A20: for v64, v1 being Element of L holds v64 "\/" H1(H1(H1(v64)) "\/" H1(v1 "\/" v64)) = v1 "\/" v64
proof
let v64, v1 be Element of L; ::_thesis: v64 "\/" H1(H1(H1(v64)) "\/" H1(v1 "\/" v64)) = v1 "\/" v64
 v64 "\/" (v1 "\/" ((v64 `) `)) = v1 "\/" v64 by A6;
hence  v64 "\/" H1(H1(H1(v64)) "\/" H1(v1 "\/" v64)) = v1 "\/" v64 by A19; ::_thesis: verum
end;
A21: for v0, v1 being Element of L holds v0 "\/" H1(v0 "\/" H1(v1 "\/" v0)) = v1 "\/" v0
proof
let v0, v1 be Element of L; ::_thesis: v0 "\/" H1(v0 "\/" H1(v1 "\/" v0)) = v1 "\/" v0
 (v0 `) ` = v0 by A18;
hence  v0 "\/" H1(v0 "\/" H1(v1 "\/" v0)) = v1 "\/" v0 by A20; ::_thesis: verum
end;
A22: for v64, v1 being Element of L holds v64 "\/" (v1 "\/" H1(v64)) = H1(v64) "\/" v64
proof
let v64, v1 be Element of L; ::_thesis: v64 "\/" (v1 "\/" H1(v64)) = H1(v64) "\/" v64
 H1(v64) "\/" H1(H1(v64) "\/" H1(v1 "\/" H1(v64))) = v1 "\/" H1(v64) by A21;
hence  v64 "\/" (v1 "\/" H1(v64)) = H1(v64) "\/" v64 by A5; ::_thesis: verum
end;
A23: for v0, v65 being Element of L holds H1(v0) "\/" H1(v0 "\/" v65) = v0 `
proof
let v0, v65 be Element of L; ::_thesis: H1(v0) "\/" H1(v0 "\/" v65) = v0 `
 (v0 `) ` = v0 by A18;
hence  H1(v0) "\/" H1(v0 "\/" v65) = v0 ` by A4; ::_thesis: verum
end;
A24: for v0, v1 being Element of L holds (v0 "\/" v1) "\/" H1(v0) = H1(v0 "\/" v1) "\/" (v0 "\/" v1)
proof
let v0, v1 be Element of L; ::_thesis: (v0 "\/" v1) "\/" H1(v0) = H1(v0 "\/" v1) "\/" (v0 "\/" v1)
 (v0 `) "\/" H1(v0 "\/" v1) = H1(v0) by A23;
hence  (v0 "\/" v1) "\/" H1(v0) = H1(v0 "\/" v1) "\/" (v0 "\/" v1) by A22; ::_thesis: verum
end;
A25: for v0, v1 being Element of L holds v0 "\/" (v1 "\/" H1(v0)) = H1(v0 "\/" v1) "\/" (v0 "\/" v1)
proof
let v0, v1 be Element of L; ::_thesis: v0 "\/" (v1 "\/" H1(v0)) = H1(v0 "\/" v1) "\/" (v0 "\/" v1)
 (v0 "\/" v1) "\/" H1(v0) = v0 "\/" (v1 "\/" H1(v0)) by ROBBINS3:def_1;
hence  v0 "\/" (v1 "\/" H1(v0)) = H1(v0 "\/" v1) "\/" (v0 "\/" v1) by A24; ::_thesis: verum
end;
A26: for v0, v1, v65 being Element of L holds v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) = H1(v0 "\/" v1) "\/" (v0 "\/" v1)
proof
let v0, v1, v65 be Element of L; ::_thesis: v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) = H1(v0 "\/" v1) "\/" (v0 "\/" v1)
 (v0 "\/" v1) "\/" (v65 "\/" H1(v0 "\/" v1)) = v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) by ROBBINS3:def_1;
hence  v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) = H1(v0 "\/" v1) "\/" (v0 "\/" v1) by A22; ::_thesis: verum
end;
A27: for v0, v1, v65 being Element of L holds v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) = v0 "\/" (v1 "\/" H1(v0))
proof
let v0, v1, v65 be Element of L; ::_thesis: v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) = v0 "\/" (v1 "\/" H1(v0))
 H1(v0 "\/" v1) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H1(v0)) by A25;
hence  v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) = v0 "\/" (v1 "\/" H1(v0)) by A26; ::_thesis: verum
end;
A28: for v1, v0, v65 being Element of L holds H1(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1)))
proof
let v1, v0, v65 be Element of L; ::_thesis: H1(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1)))
 (v0 "\/" v1) "\/" (v65 "\/" H1(v0 "\/" v1)) = v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) by ROBBINS3:def_1;
hence  H1(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) by A22; ::_thesis: verum
end;
A29: for v1, v0 being Element of L holds H1(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H1(v0))
proof
let v1, v0 be Element of L; ::_thesis: H1(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H1(v0))
now__::_thesis:_for_v65,_v1,_v0_being_Element_of_L_holds_H1(v1_"\/"_v0)_"\/"_(v0_"\/"_v1)_=_v0_"\/"_(v1_"\/"_H1(v0))
let v65, v1, v0 be Element of L; ::_thesis: H1(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H1(v0))
 v0 "\/" (v1 "\/" (v65 "\/" H1(v0 "\/" v1))) = v0 "\/" (v1 "\/" H1(v0)) by A27;
hence  H1(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H1(v0)) by A28; ::_thesis: verum
end;
hence  H1(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H1(v0)) ; ::_thesis: verum
end;
A30: for v2, v1, v65 being Element of L holds v2 "\/" (v1 "\/" H1(v2)) = (v1 "\/" v2) "\/" (v65 "\/" H1(v1 "\/" v2))
proof
let v2, v1, v65 be Element of L; ::_thesis: v2 "\/" (v1 "\/" H1(v2)) = (v1 "\/" v2) "\/" (v65 "\/" H1(v1 "\/" v2))
 H1(v1 "\/" v2) "\/" (v2 "\/" v1) = v2 "\/" (v1 "\/" H1(v2)) by A29;
hence  v2 "\/" (v1 "\/" H1(v2)) = (v1 "\/" v2) "\/" (v65 "\/" H1(v1 "\/" v2)) by A22; ::_thesis: verum
end;
A31: for v2, v1, v65 being Element of L holds v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v65 "\/" H1(v1 "\/" v2)))
proof
let v2, v1, v65 be Element of L; ::_thesis: v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v65 "\/" H1(v1 "\/" v2)))
 (v1 "\/" v2) "\/" (v65 "\/" H1(v1 "\/" v2)) = v1 "\/" (v2 "\/" (v65 "\/" H1(v1 "\/" v2))) by ROBBINS3:def_1;
hence  v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v65 "\/" H1(v1 "\/" v2))) by A30; ::_thesis: verum
end;
A32: for v2, v1 being Element of L holds v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v1 `))
proof
let v2, v1 be Element of L; ::_thesis: v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v1 `))
now__::_thesis:_for_v65,_v2,_v1_being_Element_of_L_holds_v2_"\/"_(v1_"\/"_H1(v2))_=_v1_"\/"_(v2_"\/"_H1(v1))
let v65, v2, v1 be Element of L; ::_thesis: v2 "\/" (v1 "\/" H1(v2)) = v1 "\/" (v2 "\/" H1(v1))
 v1 "\/" (v2 "\/" (v65 "\/" H1(v1 "\/" v2))) = v1 "\/" (v2 "\/" H1(v1)) by A27;
hence  v2 "\/" (v1 "\/" H1(v2)) = v1 "\/" (v2 "\/" H1(v1)) by A31; ::_thesis: verum
end;
hence  v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v1 `)) ; ::_thesis: verum
end;
A33: for v0, v1 being Element of L holds v0 "\/" (v0 `) = v1 "\/" (v0 "\/" (v1 `))
proof
let v0, v1 be Element of L; ::_thesis: v0 "\/" (v0 `) = v1 "\/" (v0 "\/" (v1 `))
 v0 "\/" (v1 "\/" (v0 `)) = v0 "\/" (v0 `) by A22;
hence  v0 "\/" (v0 `) = v1 "\/" (v0 "\/" (v1 `)) by A32; ::_thesis: verum
end;
let v1, v0 be Element of L; ::_thesis: v1 "\/" H1(v1) = v0 "\/" H1(v0)
 v1 "\/" (v0 "\/" (v1 `)) = v1 "\/" (v1 `) by A22;
hence  v1 "\/" H1(v1) = v0 "\/" H1(v0) by A33; ::_thesis: verum
end;
hence  L is with_Top by ROBBINS3:def_7; ::_thesis: verum
end;
end;

theorem :: ROBBINS4:39
for L being non empty OrthoLattStr holds
( L is Orthomodular_Lattice iff ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) )
proof
let L be non empty OrthoLattStr ; ::_thesis: ( L is Orthomodular_Lattice iff ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) )
thus  ( L is Orthomodular_Lattice implies ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) ) ; ::_thesis: ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular implies L is Orthomodular_Lattice )
assume A1: L is join-Associative ; ::_thesis: ( not L is meet-Absorbing or not L is de_Morgan or not L is Orthomodular or L is Orthomodular_Lattice )
assume A2: L is meet-Absorbing ; ::_thesis: ( not L is de_Morgan or not L is Orthomodular or L is Orthomodular_Lattice )
assume A3: L is de_Morgan ; ::_thesis: ( not L is Orthomodular or L is Orthomodular_Lattice )
A4: for x, y being Element of L holds x = x "\/" (((x `) "\/" (y `)) `)
proof
let x, y be Element of L; ::_thesis: x = x "\/" (((x `) "\/" (y `)) `)
thus x = x "\/" (x "/\" y) by A2, ROBBINS3:def_3
.= x "\/" (((x `) "\/" (y `)) `) by A3, ROBBINS1:def_23 ; ::_thesis: verum
end;
A5: for x being Element of L holds x = x "\/" ((x `) `)
proof
let x be Element of L; ::_thesis: x = x "\/" ((x `) `)
thus x = x "\/" (((x `) "\/" ((((x `) `) "\/" ((x `) `)) `)) `) by A4
.= x "\/" (((x `) "\/" ((x `) "/\" (x `))) `) by A3, ROBBINS1:def_23
.= x "\/" ((x `) `) by A2, ROBBINS3:def_3 ; ::_thesis: verum
end;
assume A6: L is Orthomodular ; ::_thesis: L is Orthomodular_Lattice
A7: for x, y being Element of L holds x "\/" y = x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `)
proof
let x, y be Element of L; ::_thesis: x "\/" y = x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `)
thus x "\/" y = x "\/" ((x `) "/\" (x "\/" y)) by A6, Def2
.= x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `) by A3, ROBBINS1:def_23 ; ::_thesis: verum
end;
A8: for x, y being Element of L holds x "\/" (((x `) "\/" y) `) = x
proof
let x, y be Element of L; ::_thesis: x "\/" (((x `) "\/" y) `) = x
thus x "\/" (((x `) "\/" y) `) = x "\/" (((x `) "\/" (((((x `) `) `) "\/" (((x `) "\/" y) `)) `)) `) by A7
.= x by A4 ; ::_thesis: verum
end;
A9: for x, y being Element of L holds x "\/" (y "\/" ((x `) `)) = y "\/" x
proof
let x, y be Element of L; ::_thesis: x "\/" (y "\/" ((x `) `)) = y "\/" x
 y "\/" x = y "\/" (x "\/" ((x `) `)) by A5;
hence  x "\/" (y "\/" ((x `) `)) = y "\/" x by A1, ROBBINS3:def_1; ::_thesis: verum
end;
A10: for x, y being Element of L holds x "\/" ((y "\/" (x `)) `) = x
proof
let x, y be Element of L; ::_thesis: x "\/" ((y "\/" (x `)) `) = x
thus x "\/" ((y "\/" (x `)) `) = x "\/" (((x `) "\/" (y "\/" (((x `) `) `))) `) by A9
.= x by A8 ; ::_thesis: verum
end;
A11: for x being Element of L holds (x `) "\/" (x `) = x `
proof
let x be Element of L; ::_thesis: (x `) "\/" (x `) = x `
thus x ` = (x `) "\/" ((x "\/" ((x `) `)) `) by A10
.= (x `) "\/" (x `) by A5 ; ::_thesis: verum
end;
A12: for x being Element of L holds ((x `) `) "\/" x = x
proof
let x be Element of L; ::_thesis: ((x `) `) "\/" x = x
((x `) `) "\/" x = x "\/" (((x `) `) "\/" ((x `) `)) by A9
.= x "\/" ((x `) `) by A11 ;
hence  ((x `) `) "\/" x = x by A5; ::_thesis: verum
end;
A13: for x being Element of L holds ((((x `) `) `) `) "\/" x = x
proof
let x be Element of L; ::_thesis: ((((x `) `) `) `) "\/" x = x
((((x `) `) `) `) "\/" x = x "\/" (((((x `) `) `) `) "\/" ((x `) `)) by A9
.= x "\/" ((x `) `) by A12 ;
hence  ((((x `) `) `) `) "\/" x = x by A5; ::_thesis: verum
end;
A14: for x being Element of L holds ((x `) `) ` = x `
proof
let x be Element of L; ::_thesis: ((x `) `) ` = x `
((x `) `) ` = (((x `) `) `) "\/" ((((((x `) `) `) `) "\/" x) `) by A8
.= (((x `) `) `) "\/" (x `) by A13 ;
hence  ((x `) `) ` = x ` by A12; ::_thesis: verum
end;
A15: for x, y being Element of L holds ((x `) `) "\/" ((y "\/" (x `)) `) = (x `) `
proof
let x, y be Element of L; ::_thesis: ((x `) `) "\/" ((y "\/" (x `)) `) = (x `) `
 (x `) ` = ((x `) `) "\/" ((y "\/" (((x `) `) `)) `) by A10;
hence  ((x `) `) "\/" ((y "\/" (x `)) `) = (x `) ` by A14; ::_thesis: verum
end;
A16: for x being Element of L holds ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) = x
proof
let x be Element of L; ::_thesis: ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) = x
x = ((((x `) `) `) `) "\/" x by A13
.= ((((x `) `) `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" ((((((x `) `) `) `) "\/" x) `)) `) by A7
.= ((((x `) `) `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" (x `)) `) by A13
.= ((x `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" (x `)) `) by A14
.= ((x `) `) "\/" ((((((x `) `) `) `) "\/" (x `)) `) by A14 ;
hence  ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) = x by A14; ::_thesis: verum
end;
A17: for x being Element of L holds (x `) ` = x
proof
let x be Element of L; ::_thesis: (x `) ` = x
thus x = ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) by A16
.= (x `) ` by A15 ; ::_thesis: verum
end;
A18: L is join-absorbing
proof
let a, b be Element of L; :: according to LATTICES:def_9 ::_thesis: a "/\" (a "\/" b) = a
a "/\" (a "\/" b) = ((a `) "\/" ((a "\/" b) `)) ` by A3, ROBBINS1:def_23
.= ((a `) "\/" ((((a `) `) "\/" b) `)) ` by A17
.= (a `) ` by A8
.= a by A17 ;
hence  a "/\" (a "\/" b) = a ; ::_thesis: verum
end;
 L is meet-Associative
proof
let a, b, c be Element of L; :: according to ROBBINS3:def_2 ::_thesis: a "/\" (b "/\" c) = b "/\" (a "/\" c)
thus a "/\" (b "/\" c) = a "/\" (((b `) "\/" (c `)) `) by A3, ROBBINS1:def_23
.= ((a `) "\/" ((((b `) "\/" (c `)) `) `)) ` by A3, ROBBINS1:def_23
.= ((a `) "\/" ((b `) "\/" (c `))) ` by A17
.= ((b `) "\/" ((a `) "\/" (c `))) ` by A1, ROBBINS3:def_1
.= ((b `) "\/" ((((a `) "\/" (c `)) `) `)) ` by A17
.= ((b `) "\/" ((a "/\" c) `)) ` by A3, ROBBINS1:def_23
.= b "/\" (a "/\" c) by A3, ROBBINS1:def_23 ; ::_thesis: verum
end;
then reconsider L9 = L as non empty Lattice-like OrthoLattStr by A1, A2, A18;
reconsider L9 = L9 as non empty Lattice-like de_Morgan join-Associative meet-Absorbing Orthomodular OrthoLattStr by A3, A6;
 L9 is with_Top ;
hence  L is Orthomodular_Lattice by A17, ROBBINS3:def_6; ::_thesis: verum
end;