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 A1: 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 x _|_ y ; :: thesis: ( not x "\/" y = Top L or x = y ` )
then A2: x [= y ` ;
assume A3: x "\/" y = Top L ; :: thesis: x = y `
thus y ` = x "\/" ((x `) "/\" (y `)) by A1, A2
.= 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 A3, Th2
.= x "\/" ((x `) "/\" x) by ROBBINS1:def 23
.= x by LATTICES:def 8 ; :: thesis: verum

end;

assume A4: 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 x "\/" ((x `) "/\" y) [= (y `) ` by ROBBINS3:def 6;
then A5: x "\/" ((x `) "/\" y) _|_ y ` ;
(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 Th2 ;
then x "\/" ((x `) "/\" y) = (y `) ` by A4, A5;
hence y = x "\/" ((x `) "/\" y) by ROBBINS3:def 6; :: thesis: verum