let L be Ortholattice; :: thesis: ( L is orthomodular iff for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b )

thus ( L is orthomodular implies for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ) by LATTICES:6, Th34; :: thesis: ( ( for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ) implies L is orthomodular )

assume A1: for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ; :: thesis: L is orthomodular

for a, b being Element of L st b [= a holds

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

thus ( L is orthomodular implies for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ) by LATTICES:6, Th34; :: thesis: ( ( for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ) implies L is orthomodular )

assume A1: for a, b being Element of L holds a "/\" ((a `) "\/" (a "/\" b)) = a "/\" b ; :: thesis: L is orthomodular

for a, b being Element of L st b [= a holds

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

proof

hence
L is orthomodular
by Th34; :: thesis: verum
let a, b be Element of L; :: thesis: ( b [= a implies a "/\" ((a `) "\/" b) = b )

assume A2: b [= a ; :: thesis: a "/\" ((a `) "\/" b) = b

hence b = a "/\" b by LATTICES:4

.= a "/\" ((a `) "\/" (a "/\" b)) by A1

.= a "/\" ((a `) "\/" b) by A2, LATTICES:4 ;

:: thesis: verum

end;assume A2: b [= a ; :: thesis: a "/\" ((a `) "\/" b) = b

hence b = a "/\" b by LATTICES:4

.= a "/\" ((a `) "\/" (a "/\" b)) by A1

.= a "/\" ((a `) "\/" b) by A2, LATTICES:4 ;

:: thesis: verum