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:6;
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:5, LATTICES:9;
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:8; :: 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