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 )

(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

(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 A6:
for a, b being Element of L st a [= b holds
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;(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

(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