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 a: 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 a, ROBBINS1:def 23;
then (((c ` ) "/\" (b ` )) ` ) "\/" a = (((c "\/" ((b ` ) ` )) ` ) ` ) "\/" a by a, ROBBINS3:def 6;
then (((c ` ) "/\" (b ` )) ` ) "\/" a = (((c "\/" b) ` ) ` ) "\/" a by a, ROBBINS3:def 6;
then (((c ` ) "/\" (b ` )) ` ) "\/" a = (c "\/" b) "\/" a by a, ROBBINS3:def 6;
then (((c ` ) "/\" (b ` )) ` ) "\/" a = a "\/" (c "\/" b) by a, LATTICES:def 4;
then (((c ` ) "/\" (b ` )) ` ) "\/" a = c "\/" (a "\/" b) by a, ROBBINS3:def 1;
hence (a "\/" b) "\/" c = (((c ` ) "/\" (b ` )) ` ) "\/" a by a, LATTICES:def 4; :: thesis: verum

end;

thus for a, b being Element of L holds a = a "/\" (a "\/" b) by a, 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 a, ROBBINS1:def 23
.= a "\/" (((b ` ) "\/" b) ` ) by a, ROBBINS3:def 6
.= a "\/" ((b "\/" (b ` )) ` ) by a, LATTICES:def 4
.= a "\/" ((a "\/" (a ` )) ` ) by a, ROBBINS3:def 7
.= a "\/" ((((a ` ) ` ) "\/" (a ` )) ` ) by a, ROBBINS3:def 6
.= a "\/" ((a ` ) "/\" a) by a, ROBBINS1:def 23
.= ((a ` ) "/\" a) "\/" a by a, LATTICES:def 4
.= a by a, LATTICES:def 8 ; :: thesis: verum

end;

assume z1: 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 z2: 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 z3: for a, b being Element of L holds a = a "\/" (b "/\" (b ` )) ; :: thesis: L is Ortholattice
a: 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 z3
.= a by z2 ; :: thesis: verum

end;

b: 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 z1;
then (a "\/" (b "/\" (b ` ))) "\/" (b "/\" (b ` )) = (((b "/\" (b ` )) ` ) ` ) "\/" a by a;
then a "\/" (b "/\" (b ` )) = (((b "/\" (b ` )) ` ) ` ) "\/" a by z3;
hence a = (((b "/\" (b ` )) ` ) ` ) "\/" a by z3; :: thesis: verum

end;

c: 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 b
.= ((a "/\" (a ` )) ` ) ` by z3 ; :: thesis: verum

end;

d: 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 b;
hence a = (b "/\" (b ` )) "\/" a by c; :: thesis: verum

end;

e: 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 z3;
hence a "/\" (a ` ) = b "/\" (b ` ) by d; :: thesis: verum

end;

f: 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 z1;
hence a "\/" b = (((b ` ) "/\" (a ` )) ` ) "\/" (a "/\" (a ` )) by d
.= ((b ` ) "/\" (a ` )) ` by z3 ;
:: thesis: verum

end;

k1: 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 f;
hence b "\/" a = (((b ` ) "/\" ((a "/\" (a ` )) ` )) ` ) "\/" a by d
.= (a "\/" (a "/\" (a ` ))) "\/" b by z1
.= a "\/" b by z3 ;
:: thesis: verum

end;

k2: 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 z1
.= (b "\/" c) "\/" a by f
.= a "\/" (b "\/" c) by k1, LATTICES:def 4 ; :: thesis: verum

end;

l1: L is involutive

proof

let a be Element of L; :: according to ROBBINS3:def 6 :: thesis: (a ` ) ` = a
a2: a ` = (a ` ) "/\" ((a ` ) "\/" a) by z2;
(a ` ) "\/" a = ((a ` ) "/\" ((a ` ) ` )) ` by f;
hence (a ` ) ` = ((a ` ) "/\" ((a ` ) ` )) "\/" a by f, a2
.= a by d ;
:: thesis: verum

end;

l2: 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 k1, LATTICES:def 4
.= ((((a ` ) ` ) "/\" ((b ` ) ` )) ` ) ` by f
.= ((a ` ) ` ) "/\" ((b ` ) ` ) by l1, ROBBINS3:def 6
.= ((a ` ) ` ) "/\" b by l1, ROBBINS3:def 6
.= a "/\" b by l1, ROBBINS3:def 6 ; :: thesis: verum

end;

l3: 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 e;
then ((a ` ) "/\" ((a ` ) ` )) ` = (b ` ) "\/" b by f;
then (a ` ) "\/" a = (b ` ) "\/" b by f;
then (a ` ) "\/" a = b "\/" (b ` ) by k1, LATTICES:def 4;
hence a "\/" (a ` ) = b "\/" (b ` ) by k1, LATTICES:def 4; :: thesis: verum

end;

k3: L is join-absorbing by z2, LATTICES:def 9;
k5: 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 l2, ROBBINS1:def 23
.= ((a ` ) "\/" ((((b ` ) "\/" (c ` )) ` ) ` )) ` by l2, ROBBINS1:def 23
.= ((a ` ) "\/" ((b ` ) "\/" (c ` ))) ` by l1, ROBBINS3:def 6
.= (((a ` ) "\/" (b ` )) "\/" (c ` )) ` by k2, LATTICES:def 5
.= (((((a ` ) "\/" (b ` )) ` ) ` ) "\/" (c ` )) ` by l1, ROBBINS3:def 6
.= (((a "/\" b) ` ) "\/" (c ` )) ` by l2, ROBBINS1:def 23
.= (a "/\" b) "/\" c by l2, ROBBINS1:def 23 ; :: thesis: verum

end;

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 f
.= ((b ` ) "/\" ((((a ` ) "\/" (b ` )) ` ) ` )) ` by l2, ROBBINS1:def 23
.= ((b ` ) "/\" ((a ` ) "\/" (b ` ))) ` by l1, ROBBINS3:def 6
.= ((b ` ) "/\" ((b ` ) "\/" (a ` ))) ` by k1, LATTICES:def 4
.= (b ` ) ` by z2
.= b by l1, ROBBINS3:def 6 ; :: thesis: verum

end;

hence L is Ortholattice by l1, l2, l3, k1, k2, k3, k5; :: thesis: verum