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 ) :: thesis: ( ( for a, b being Element of L holds a "/\" ((a ` ) "\/" (a "/\" b)) = a "/\" b ) implies L is orthomodular )

proof

assume A1: L is orthomodular ; :: thesis: for a, b being Element of L holds a "/\" ((a ` ) "\/" (a "/\" b)) = a "/\" b
let a, b be Element of L; :: thesis: a "/\" ((a ` ) "\/" (a "/\" b)) = a "/\" b
a "/\" b [= a by LATTICES:23;
hence a "/\" ((a ` ) "\/" (a "/\" b)) = a "/\" b by A1, Th34; :: thesis: verum

end;

assume A2: 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 A3: b [= a ; :: thesis: a "/\" ((a ` ) "\/" b) = b
hence b = a "/\" b by LATTICES:21
.= a "/\" ((a ` ) "\/" (a "/\" b)) by A2
.= a "/\" ((a ` ) "\/" b) by A3, LATTICES:21 ;
:: thesis: verum

end;

hence L is orthomodular by Th34; :: thesis: verum