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 )

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 `))

hence L is Orthomodular_Lattice by A7, Th36; :: thesis: verum

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 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 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 `))

end;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

thus
for a, b being Element of L holds a = a "\/" (b "/\" (b `))
by A1, Th3; :: thesis: verum
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;( (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

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

for a, c being Element of L holds a = a "/\" (a "\/" c)
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;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

proof

then
L is Ortholattice
by A4, A6, Th3;
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;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

hence L is Orthomodular_Lattice by A7, Th36; :: thesis: verum