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
.= ((((a `) `) "/\" ((b `) `)) `) ` by A9
.= ((a `) `) "/\" ((b `) `) by A10
.= ((a `) `) "/\" b by A10
.= a "/\" b by A10 ; :: 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
.= ((b `) "/\" ((a `) "\/" (b `))) ` by A10
.= ((b `) "/\" ((b `) "\/" (a `))) ` by A11
.= (b `) ` by A3
.= b by A10 ; :: 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 ; :: 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
.= ((a `) "\/" ((((b `) "\/" (c `)) `) `)) ` by A12
.= ((a `) "\/" ((b `) "\/" (c `))) ` by A10
.= (((a `) "\/" (b `)) "\/" (c `)) ` by A14
.= (((((a `) "\/" (b `)) `) `) "\/" (c `)) ` by A10
.= (((a "/\" b) `) "\/" (c `)) ` by A12
.= (a "/\" b) "/\" c by A12 ; :: 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;
hence a "\/" (a `) = b "\/" (b `) by A11; :: thesis: verum

end;

L is join-absorbing by A3;
hence L is Ortholattice by A11, A14, A10, A12, A17, A15, A13; :: thesis: verum