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

proof

assume z1: L is orthomodular ; :: thesis: for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
a = b `
let x, y be Element of L; :: thesis: ( x _|_ y & x "\/" y = Top L implies x = y ` )
assume z2: x _|_ y ; :: thesis: ( not x "\/" y = Top L or x = y ` )
assume z3: x "\/" y = Top L ; :: thesis: x = y `
x [= y ` by z2, orthogonal;
hence y ` = x "\/" ((x ` ) "/\" (y ` )) by z1, DefModular
.= x "\/" ((((x ` ) ` ) "\/" ((y ` ) ` )) ` ) by ROBBINS1:def 23
.= x "\/" ((x "\/" ((y ` ) ` )) ` ) by ROBBINS3:def 6
.= x "\/" ((x "\/" y) ` ) by ROBBINS3:def 6
.= x "\/" ((((x ` ) ` ) "\/" (x ` )) ` ) by yy, z3
.= x "\/" ((x ` ) "/\" x) by ROBBINS1:def 23
.= x by LATTICES:def 8 ;
:: thesis: verum

end;

assume z: for a, b being Element of L st a _|_ b & a "\/" b = Top 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: (y ` ) "\/" (x "\/" ((x ` ) "/\" y)) = ((y ` ) "\/" x) "\/" ((x ` ) "/\" y) by LATTICES:def 5
.= ((y ` ) "\/" ((x ` ) ` )) "\/" ((x ` ) "/\" y) by ROBBINS3:def 6
.= ((((y ` ) "\/" ((x ` ) ` )) ` ) ` ) "\/" ((x ` ) "/\" y) by ROBBINS3:def 6
.= ((y "/\" (x ` )) ` ) "\/" ((x ` ) "/\" y) by ROBBINS1:def 23
.= Top L by yy ;
x "\/" ((x ` ) "/\" y) _|_ y ` by a, orthogonal;
then x "\/" ((x ` ) "/\" y) = (y ` ) ` by b, z;
hence y = x "\/" ((x ` ) "/\" y) by ROBBINS3:def 6; :: thesis: verum