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 )

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 A5: ((x "\/" ((x `) "/\" y)) `) ` [= y by ROBBINS3:def 6;

((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 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 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 A4:
for a, b being Element of L st b ` [= a & a "/\" b = Bottom L holds
assume A1:
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 A2: y ` [= x ; :: thesis: ( not x "/\" y = Bottom L or x = y ` )

assume A3: x "/\" y = Bottom L ; :: thesis: x = y `

thus x = (y `) "\/" (((y `) `) "/\" x) by A1, A2

.= (y `) "\/" (y "/\" x) by ROBBINS3:def 6

.= y ` by A3 ; :: thesis: verum

end;a = b `

let x, y be Element of L; :: thesis: ( y ` [= x & x "/\" y = Bottom L implies x = y ` )

assume A2: y ` [= x ; :: thesis: ( not x "/\" y = Bottom L or x = y ` )

assume A3: x "/\" y = Bottom L ; :: thesis: x = y `

thus x = (y `) "\/" (((y `) `) "/\" x) by A1, A2

.= (y `) "\/" (y "/\" x) by ROBBINS3:def 6

.= y ` by A3 ; :: 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 A5: ((x "\/" ((x `) "/\" y)) `) ` [= y by ROBBINS3:def 6;

((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 Th2 ;

then ((x "\/" ((x `) "/\" y)) `) ` = y by A4, A5;

hence y = x "\/" ((x `) "/\" y) by ROBBINS3:def 6; :: thesis: verum