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 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;
assume A4: 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 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