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 A1: 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 A2: a [= b ; :: thesis: (a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` ))
( a "/\" b [= a "\/" b & b "/\" (a ` ) [= a "\/" b ) by FILTER_0:3, LATTICES:23;
then A3: (a "/\" b) "\/" (b "/\" (a ` )) [= a "\/" b by FILTER_0:6;
( a "/\" b [= b "\/" (a ` ) & b "/\" (a ` ) [= b "\/" (a ` ) ) by FILTER_0:3, LATTICES:23;
then (a "/\" b) "\/" (b "/\" (a ` )) [= b "\/" (a ` ) by FILTER_0:6;
then A4: (a "/\" b) "\/" (b "/\" (a ` )) [= (a "\/" b) "/\" (b "\/" (a ` )) by A3, FILTER_0:7;
A5: (a "\/" b) "/\" (b "\/" (a ` )) [= a "\/" b by LATTICES:23;
a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a ` )) by A1, Th36
.= (b "/\" a) "\/" ((a "\/" b) "/\" (a ` )) by A2, LATTICES:def 3
.= (b "/\" a) "\/" (b "/\" (a ` )) by A2, LATTICES:def 3 ;
hence (a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` )) by A4, A5, LATTICES:26; :: thesis: verum

end;

assume A6: 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 A7: a [= b ; :: thesis: b = a "\/" ((a ` ) "/\" b)
then (a "\/" b) "/\" (b "\/" (a ` )) = (a "/\" b) "\/" (b "/\" (a ` )) by A6
.= a "\/" ((a ` ) "/\" b) by A7, LATTICES:21 ;
hence a "\/" ((a ` ) "/\" b) = b "/\" (b "\/" (a ` )) by A7, LATTICES:def 3
.= b by LATTICES:def 9 ;
:: thesis: verum