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 )

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

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 A4:
for a, b being Element of L st a _|_ b & a "\/" b = Top L holds
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;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

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