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 )

proof

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;

assume A2: for a, b being Element of L st b [= a holds
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