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 a: 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 ` )) ) )
thus for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c ` ) "/\" (b ` )) ` ) "\/" a by 3ort, a; :: 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: a "\/" b [= ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a ` ))

proof

c: a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a ` )) by a, dziw;
a "/\" (a "\/" b) [= (a "\/" c) "/\" (a "\/" b) by a, LATTICES:22, LATTICES:27;
then (a "\/" b) "/\" a [= (a "\/" c) "/\" (a "\/" b) by a, LATTICES:def 6;
then (a "\/" b) "/\" a [= (a "\/" b) "/\" (a "\/" c) by a, LATTICES:def 6;
then ((a "\/" b) "/\" (a ` )) "\/" ((a "\/" b) "/\" a) [= ((a "\/" b) "/\" (a ` )) "\/" ((a "\/" b) "/\" (a "\/" c)) by a, FILTER_0:1;
then ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a ` )) [= ((a "\/" b) "/\" (a ` )) "\/" ((a "\/" b) "/\" (a "\/" c)) by a, LATTICES:def 4;
hence a "\/" b [= ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a ` )) by c, a, LATTICES:def 4; :: thesis: verum

end;

((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a ` )) [= a "\/" b

proof

b: (a "\/" b) "/\" (a ` ) [= a "\/" b by a, LATTICES:23;
(a "\/" b) "/\" (a "\/" c) [= a "\/" b by a, LATTICES:23;
hence ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a ` )) [= a "\/" b by b, a, FILTER_0:6; :: thesis: verum

end;

hence a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" (a ` )) by A, a, LATTICES:26; :: thesis: verum

end;

thus for a, b being Element of L holds a = a "\/" (b "/\" (b ` )) by 3ort, a; :: thesis: verum

end;

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

end;

B: L is Ortholattice by z1, z3, A, 3ort;
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 z2;
hence a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a ` )) by z3; :: thesis: verum

end;

hence L is Orthomodular_Lattice by dziw, B; :: thesis: verum