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

proof

assume z1: L is orthomodular ; :: thesis: for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
a = b `
let x, y be Element of L; :: thesis: ( y ` [= x & x "/\" y = Bottom L implies x = y ` )
assume z2: y ` [= x ; :: thesis: ( not x "/\" y = Bottom L or x = y ` )
assume z3: x "/\" y = Bottom L ; :: thesis: x = y `
thus x = (y ` ) "\/" (((y ` ) ` ) "/\" x) by z1, z2, DefModular
.= (y ` ) "\/" (y "/\" x) by ROBBINS3:def 6
.= y ` by z3, LATTICES:39 ; :: thesis: verum

end;

assume z: for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
a = b ` ; :: thesis: L is orthomodular
let x, y be Element of L; :: according to ROBBINS4:def 1 :: thesis: ( x [= y implies y = x "\/" ((x ` ) "/\" y) )
assume x [= y ; :: thesis: y = x "\/" ((x ` ) "/\" y)
then x "\/" ((x ` ) "/\" y) [= y "\/" ((x ` ) "/\" y) by FILTER_0:1;
then x "\/" ((x ` ) "/\" y) [= y by LATTICES:def 8;
then a: ((x "\/" ((x ` ) "/\" y)) ` ) ` [= y by ROBBINS3:def 6;
b: ((x "\/" ((x ` ) "/\" y)) ` ) "/\" y = y "/\" ((((x ` ) ` ) "\/" ((x ` ) "/\" y)) ` ) by ROBBINS3:def 6
.= y "/\" ((((x ` ) ` ) "\/" ((((x ` ) "/\" y) ` ) ` )) ` ) by ROBBINS3:def 6
.= y "/\" ((x ` ) "/\" (((x ` ) "/\" y) ` )) by ROBBINS1:def 23
.= y "/\" ((x ` ) "/\" (((((x ` ) ` ) "\/" (y ` )) ` ) ` )) by ROBBINS1:def 23
.= y "/\" ((x ` ) "/\" (((x ` ) ` ) "\/" (y ` ))) by ROBBINS3:def 6
.= y "/\" ((x ` ) "/\" (x "\/" (y ` ))) by ROBBINS3:def 6
.= (y "/\" (x ` )) "/\" (x "\/" (y ` )) by LATTICES:def 7
.= (((y ` ) "\/" ((x ` ) ` )) ` ) "/\" (x "\/" (y ` )) by ROBBINS1:def 23
.= ((x "\/" (y ` )) ` ) "/\" (x "\/" (y ` )) by ROBBINS3:def 6
.= Bottom L by yy ;
((x "\/" ((x ` ) "/\" y)) ` ) ` = y by a, b, z;
hence y = x "\/" ((x ` ) "/\" y) by ROBBINS3:def 6; :: thesis: verum