let L be Ortholattice; :: thesis: ( L is orthomodular iff for a, b being Element of L st b [= a holds

a "/\" ((a `) "\/" b) = b )

thus ( L is orthomodular implies for a, b being Element of L st b [= a holds

a "/\" ((a `) "\/" b) = b ) :: thesis: ( ( for a, b being Element of L st b [= a holds

a "/\" ((a `) "\/" b) = b ) implies L is orthomodular )

a "/\" ((a `) "\/" b) = b ; :: thesis: L is orthomodular

let a, b be Element of L; :: according to ROBBINS4:def 1 :: thesis: ( a [= b implies b = a "\/" ((a `) "/\" b) )

assume a [= b ; :: thesis: b = a "\/" ((a `) "/\" b)

then b ` [= a ` by Th4;

then b ` = (a `) "/\" (((a `) `) "\/" (b `)) by A2

.= (a `) "/\" (((((a `) `) "\/" (b `)) `) `) by ROBBINS3:def 6

.= (a `) "/\" (((a `) "/\" b) `) by ROBBINS1:def 23

.= (((a `) `) "\/" ((((a `) "/\" b) `) `)) ` by ROBBINS1:def 23

.= (a "\/" ((((a `) "/\" b) `) `)) ` by ROBBINS3:def 6

.= (a "\/" ((a `) "/\" b)) ` by ROBBINS3:def 6 ;

then (b `) ` = a "\/" ((a `) "/\" b) by ROBBINS3:def 6;

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

a "/\" ((a `) "\/" b) = b )

thus ( L is orthomodular implies for a, b being Element of L st b [= a holds

a "/\" ((a `) "\/" b) = b ) :: thesis: ( ( for a, b being Element of L st b [= a holds

a "/\" ((a `) "\/" b) = b ) implies L is orthomodular )

proof

assume A2:
for a, b being Element of L st b [= a holds
assume A1:
L is orthomodular
; :: thesis: for a, b being Element of L st b [= a holds

a "/\" ((a `) "\/" b) = b

let a, b be Element of L; :: thesis: ( b [= a implies a "/\" ((a `) "\/" b) = b )

assume b [= a ; :: thesis: a "/\" ((a `) "\/" b) = b

then a ` [= b ` by Th4;

then b ` = (a `) "\/" (((a `) `) "/\" (b `)) by A1

.= (a `) "\/" (a "/\" (b `)) by ROBBINS3:def 6

.= (a `) "\/" (((a `) "\/" ((b `) `)) `) by ROBBINS1:def 23

.= (a `) "\/" (((a `) "\/" b) `) by ROBBINS3:def 6

.= (((a `) "\/" (((a `) "\/" b) `)) `) ` by ROBBINS3:def 6

.= (a "/\" ((a `) "\/" b)) ` by ROBBINS1:def 23 ;

then (b `) ` = a "/\" ((a `) "\/" b) by ROBBINS3:def 6;

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

end;a "/\" ((a `) "\/" b) = b

let a, b be Element of L; :: thesis: ( b [= a implies a "/\" ((a `) "\/" b) = b )

assume b [= a ; :: thesis: a "/\" ((a `) "\/" b) = b

then a ` [= b ` by Th4;

then b ` = (a `) "\/" (((a `) `) "/\" (b `)) by A1

.= (a `) "\/" (a "/\" (b `)) by ROBBINS3:def 6

.= (a `) "\/" (((a `) "\/" ((b `) `)) `) by ROBBINS1:def 23

.= (a `) "\/" (((a `) "\/" b) `) by ROBBINS3:def 6

.= (((a `) "\/" (((a `) "\/" b) `)) `) ` by ROBBINS3:def 6

.= (a "/\" ((a `) "\/" b)) ` by ROBBINS1:def 23 ;

then (b `) ` = a "/\" ((a `) "\/" b) by ROBBINS3:def 6;

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

a "/\" ((a `) "\/" b) = b ; :: thesis: L is orthomodular

let a, b be Element of L; :: according to ROBBINS4:def 1 :: thesis: ( a [= b implies b = a "\/" ((a `) "/\" b) )

assume a [= b ; :: thesis: b = a "\/" ((a `) "/\" b)

then b ` [= a ` by Th4;

then b ` = (a `) "/\" (((a `) `) "\/" (b `)) by A2

.= (a `) "/\" (((((a `) `) "\/" (b `)) `) `) by ROBBINS3:def 6

.= (a `) "/\" (((a `) "/\" b) `) by ROBBINS1:def 23

.= (((a `) `) "\/" ((((a `) "/\" b) `) `)) ` by ROBBINS1:def 23

.= (a "\/" ((((a `) "/\" b) `) `)) ` by ROBBINS3:def 6

.= (a "\/" ((a `) "/\" b)) ` by ROBBINS3:def 6 ;

then (b `) ` = a "\/" ((a `) "/\" b) by ROBBINS3:def 6;

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