let L be Ortholattice; :: thesis: ( L is orthomodular iff for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) )
thus ( L is orthomodular implies for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) ) :: thesis: ( ( for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) ) implies L is orthomodular )

proof

assume A1: L is orthomodular ; :: thesis: for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `))
let a, b be Element of L; :: thesis: a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `))
a "\/" b = a "\/" ((a "\/" b) "/\" (a `)) by A1, Th6;
hence a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) by LATTICES:def 9; :: thesis: verum

end;

assume A2: for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) ; :: 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 A3: x [= y ; :: thesis: y = x "\/" ((x `) "/\" y)
hence y = x "\/" y
.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" (x `)) by A2
.= (y "/\" x) "\/" ((x "\/" y) "/\" (x `)) by A3
.= (y "/\" x) "\/" (y "/\" (x `)) by A3
.= x "\/" ((x `) "/\" y) by A3, LATTICES:4 ;
:: thesis: verum