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:23;
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:22, LATTICES:27;
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:26; :: 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