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:6;
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:6;
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:6;
a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) by A1, Th36
.= (b "/\" a) "\/" ((a "\/" b) "/\" (a `)) by A2
.= (b "/\" a) "\/" (b "/\" (a `)) by A2 ;
hence (a "\/" b) "/\" (b "\/" (a `)) = (a "/\" b) "\/" (b "/\" (a `)) by A4, A5, LATTICES:8; :: 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:4 ;
hence a "\/" ((a `) "/\" b) = b "/\" (b "\/" (a `)) by A7
.= b by LATTICES:def 9 ;
:: thesis: verum