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 a: 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 twDual, a; :: thesis: verum

end;

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

end;

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