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 )

let x, y be Element of L; :: according to ROBBINS4:def 1 :: thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )

assume A3: x [= y ; :: thesis: y = x "\/" ((x `) "/\" y)

hence y = x "\/" y

.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" (x `)) by A2

.= (y "/\" x) "\/" ((x "\/" y) "/\" (x `)) by A3

.= (y "/\" x) "\/" (y "/\" (x `)) by A3

.= x "\/" ((x `) "/\" y) by A3, LATTICES:4 ;

:: thesis: verum

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 A2:
for a, b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `))
; :: thesis: L is orthomodular
assume A1:
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 A1, Th6;

hence a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) by LATTICES:def 9; :: thesis: verum

end;let a, b be Element of L; :: thesis: a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `))

a "\/" b = a "\/" ((a "\/" b) "/\" (a `)) by A1, Th6;

hence a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" (a `)) by LATTICES:def 9; :: thesis: verum

let x, y be Element of L; :: according to ROBBINS4:def 1 :: thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )

assume A3: x [= y ; :: thesis: y = x "\/" ((x `) "/\" y)

hence y = x "\/" y

.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" (x `)) by A2

.= (y "/\" x) "\/" ((x "\/" y) "/\" (x `)) by A3

.= (y "/\" x) "\/" (y "/\" (x `)) by A3

.= x "\/" ((x `) "/\" y) by A3, LATTICES:4 ;

:: thesis: verum