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
proof
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;
hence L is orthomodular by Th34; :: thesis: verum