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

proof

assume z1: L is orthomodular ; :: thesis: for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` ))
let a, b be Element of L; :: thesis: ( a [= b implies (a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` )) )
assume z2: a [= b ; :: thesis: (a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` ))
b: a "/\" b [= a "\/" b by FILTER_0:3, LATTICES:23;
c: a "/\" b [= b "\/" (a ` ) by FILTER_0:3, LATTICES:23;
e: b "/\" (a ` ) [= b "\/" (a ` ) by FILTER_0:3, LATTICES:23;
f: b "/\" (a ` ) [= a "\/" b by FILTER_0:3, LATTICES:23;
g: (a "/\" b) "\/" (b "/\" (a ` )) [= a "\/" b by b, f, FILTER_0:6;
(a "/\" b) "\/" (b "/\" (a ` )) [= b "\/" (a ` ) by c, e, FILTER_0:6;
then B: (a "/\" b) "\/" (b "/\" (a ` )) [= (a "\/" b) "/\" (b "\/" (a ` )) by g, FILTER_0:7;
h: a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a ` )) by z1, dziw
.= (b "/\" a) "\/" ((a "\/" b) "/\" (a ` )) by z2, LATTICES:def 3
.= (b "/\" a) "\/" (b "/\" (a ` )) by z2, LATTICES:def 3 ;
(a "\/" b) "/\" (b "\/" (a ` )) [= a "\/" b by LATTICES:23;
hence (a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` )) by B, h, LATTICES:26; :: thesis: verum

end;

assume z1: for a, b being Element of L st a [= b holds
(a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` )) ; :: thesis: L is orthomodular
let a be Element of L; :: according to ROBBINS4:def 1 :: thesis: for y being Element of L st a [= y holds
y = a "\/" ((a ` ) "/\" y)
let b be Element of L; :: thesis: ( a [= b implies b = a "\/" ((a ` ) "/\" b) )
assume z2: a [= b ; :: thesis: b = a "\/" ((a ` ) "/\" b)
then (a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` )) by z1
.= a "\/" ((a ` ) "/\" b) by z2, LATTICES:21 ;
hence a "\/" ((a ` ) "/\" b) = b "/\" (b "\/" (a ` )) by z2, LATTICES:def 3
.= b by LATTICES:def 9 ;
:: thesis: verum