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
set x = a "/\" (a ` );
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