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 z: 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 tw1, z;
hence a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a ` )) by LATTICES:def 9; :: thesis: verum

end;

assume z1: 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 z2: x [= y ; :: thesis: y = x "\/" ((x ` ) "/\" y)
hence y = x "\/" y by LATTICES:def 3
.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" (x ` )) by z1
.= (y "/\" x) "\/" ((x "\/" y) "/\" (x ` )) by z2, LATTICES:def 3
.= (y "/\" x) "\/" (y "/\" (x ` )) by z2, LATTICES:def 3
.= x "\/" ((x ` ) "/\" y) by z2, LATTICES:21 ;
:: thesis: verum