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 ;
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 ;
:: thesis: verum