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

proof

assume z1: L is orthomodular ; :: thesis: for a, b being Element of L st b [= a holds
a "/\" ((a ` ) "\/" b) = b
let a, b be Element of L; :: thesis: ( b [= a implies a "/\" ((a ` ) "\/" b) = b )
assume b [= a ; :: thesis: a "/\" ((a ` ) "\/" b) = b
then a ` [= b ` by theo;
then b ` = (a ` ) "\/" (((a ` ) ` ) "/\" (b ` )) by DefModular, z1
.= (a ` ) "\/" (a "/\" (b ` )) by ROBBINS3:def 6
.= (a ` ) "\/" (((a ` ) "\/" ((b ` ) ` )) ` ) by ROBBINS1:def 23
.= (a ` ) "\/" (((a ` ) "\/" b) ` ) by ROBBINS3:def 6
.= (((a ` ) "\/" (((a ` ) "\/" b) ` )) ` ) ` by ROBBINS3:def 6
.= (a "/\" ((a ` ) "\/" b)) ` by ROBBINS1:def 23 ;
then (b ` ) ` = a "/\" ((a ` ) "\/" b) by ROBBINS3:def 6;
hence a "/\" ((a ` ) "\/" b) = b by ROBBINS3:def 6; :: thesis: verum

end;

assume z1: for a, b being Element of L st b [= a holds
a "/\" ((a ` ) "\/" b) = b ; :: thesis: L is orthomodular
let a, b be Element of L; :: according to ROBBINS4:def 1 :: thesis: ( a [= b implies b = a "\/" ((a ` ) "/\" b) )
assume a [= b ; :: thesis: b = a "\/" ((a ` ) "/\" b)
then b ` [= a ` by theo;
then b ` = (a ` ) "/\" (((a ` ) ` ) "\/" (b ` )) by z1
.= (a ` ) "/\" (((((a ` ) ` ) "\/" (b ` )) ` ) ` ) by ROBBINS3:def 6
.= (a ` ) "/\" (((a ` ) "/\" b) ` ) by ROBBINS1:def 23
.= (((a ` ) ` ) "\/" ((((a ` ) "/\" b) ` ) ` )) ` by ROBBINS1:def 23
.= (a "\/" ((((a ` ) "/\" b) ` ) ` )) ` by ROBBINS3:def 6
.= (a "\/" ((a ` ) "/\" b)) ` by ROBBINS3:def 6 ;
then (b ` ) ` = a "\/" ((a ` ) "/\" b) by ROBBINS3:def 6;
hence b = a "\/" ((a ` ) "/\" b) by ROBBINS3:def 6; :: thesis: verum