let L be non empty OrthoLattStr ; :: thesis: ( L is Orthomodular_Lattice iff ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) )

thus ( L is Orthomodular_Lattice implies ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) ) ; :: thesis: ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular implies L is Orthomodular_Lattice )

assume A1: L is join-Associative ; :: thesis: ( not L is meet-Absorbing or not L is de_Morgan or not L is Orthomodular or L is Orthomodular_Lattice )

assume A2: L is meet-Absorbing ; :: thesis: ( not L is de_Morgan or not L is Orthomodular or L is Orthomodular_Lattice )

assume A3: L is de_Morgan ; :: thesis: ( not L is Orthomodular or L is Orthomodular_Lattice )

A4: for x, y being Element of L holds x = x "\/" (((x `) "\/" (y `)) `)

A7: for x, y being Element of L holds x "\/" y = x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `)

reconsider L9 = L9 as non empty Lattice-like de_Morgan join-Associative meet-Absorbing Orthomodular OrthoLattStr by A3, A6;

L9 is with_Top ;

hence L is Orthomodular_Lattice by A17, ROBBINS3:def 6; :: thesis: verum

thus ( L is Orthomodular_Lattice implies ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) ) ; :: thesis: ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular implies L is Orthomodular_Lattice )

assume A1: L is join-Associative ; :: thesis: ( not L is meet-Absorbing or not L is de_Morgan or not L is Orthomodular or L is Orthomodular_Lattice )

assume A2: L is meet-Absorbing ; :: thesis: ( not L is de_Morgan or not L is Orthomodular or L is Orthomodular_Lattice )

assume A3: L is de_Morgan ; :: thesis: ( not L is Orthomodular or L is Orthomodular_Lattice )

A4: for x, y being Element of L holds x = x "\/" (((x `) "\/" (y `)) `)

proof

A5:
for x being Element of L holds x = x "\/" ((x `) `)
let x, y be Element of L; :: thesis: x = x "\/" (((x `) "\/" (y `)) `)

thus x = x "\/" (x "/\" y) by A2

.= x "\/" (((x `) "\/" (y `)) `) by A3 ; :: thesis: verum

end;thus x = x "\/" (x "/\" y) by A2

.= x "\/" (((x `) "\/" (y `)) `) by A3 ; :: thesis: verum

proof

assume A6:
L is Orthomodular
; :: thesis: L is Orthomodular_Lattice
let x be Element of L; :: thesis: x = x "\/" ((x `) `)

thus x = x "\/" (((x `) "\/" ((((x `) `) "\/" ((x `) `)) `)) `) by A4

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

.= x "\/" ((x `) `) by A2 ; :: thesis: verum

end;thus x = x "\/" (((x `) "\/" ((((x `) `) "\/" ((x `) `)) `)) `) by A4

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

.= x "\/" ((x `) `) by A2 ; :: thesis: verum

A7: for x, y being Element of L holds x "\/" y = x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `)

proof

A8:
for x, y being Element of L holds x "\/" (((x `) "\/" y) `) = x
let x, y be Element of L; :: thesis: x "\/" y = x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `)

thus x "\/" y = x "\/" ((x `) "/\" (x "\/" y)) by A6

.= x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `) by A3 ; :: thesis: verum

end;thus x "\/" y = x "\/" ((x `) "/\" (x "\/" y)) by A6

.= x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `) by A3 ; :: thesis: verum

proof

A9:
for x, y being Element of L holds x "\/" (y "\/" ((x `) `)) = y "\/" x
let x, y be Element of L; :: thesis: x "\/" (((x `) "\/" y) `) = x

thus x "\/" (((x `) "\/" y) `) = x "\/" (((x `) "\/" (((((x `) `) `) "\/" (((x `) "\/" y) `)) `)) `) by A7

.= x by A4 ; :: thesis: verum

end;thus x "\/" (((x `) "\/" y) `) = x "\/" (((x `) "\/" (((((x `) `) `) "\/" (((x `) "\/" y) `)) `)) `) by A7

.= x by A4 ; :: thesis: verum

proof

A10:
for x, y being Element of L holds x "\/" ((y "\/" (x `)) `) = x
let x, y be Element of L; :: thesis: x "\/" (y "\/" ((x `) `)) = y "\/" x

y "\/" x = y "\/" (x "\/" ((x `) `)) by A5;

hence x "\/" (y "\/" ((x `) `)) = y "\/" x by A1; :: thesis: verum

end;y "\/" x = y "\/" (x "\/" ((x `) `)) by A5;

hence x "\/" (y "\/" ((x `) `)) = y "\/" x by A1; :: thesis: verum

proof

A11:
for x being Element of L holds (x `) "\/" (x `) = x `
let x, y be Element of L; :: thesis: x "\/" ((y "\/" (x `)) `) = x

thus x "\/" ((y "\/" (x `)) `) = x "\/" (((x `) "\/" (y "\/" (((x `) `) `))) `) by A9

.= x by A8 ; :: thesis: verum

end;thus x "\/" ((y "\/" (x `)) `) = x "\/" (((x `) "\/" (y "\/" (((x `) `) `))) `) by A9

.= x by A8 ; :: thesis: verum

proof

A12:
for x being Element of L holds ((x `) `) "\/" x = x
let x be Element of L; :: thesis: (x `) "\/" (x `) = x `

thus x ` = (x `) "\/" ((x "\/" ((x `) `)) `) by A10

.= (x `) "\/" (x `) by A5 ; :: thesis: verum

end;thus x ` = (x `) "\/" ((x "\/" ((x `) `)) `) by A10

.= (x `) "\/" (x `) by A5 ; :: thesis: verum

proof

A13:
for x being Element of L holds ((((x `) `) `) `) "\/" x = x
let x be Element of L; :: thesis: ((x `) `) "\/" x = x

((x `) `) "\/" x = x "\/" (((x `) `) "\/" ((x `) `)) by A9

.= x "\/" ((x `) `) by A11 ;

hence ((x `) `) "\/" x = x by A5; :: thesis: verum

end;((x `) `) "\/" x = x "\/" (((x `) `) "\/" ((x `) `)) by A9

.= x "\/" ((x `) `) by A11 ;

hence ((x `) `) "\/" x = x by A5; :: thesis: verum

proof

A14:
for x being Element of L holds ((x `) `) ` = x `
let x be Element of L; :: thesis: ((((x `) `) `) `) "\/" x = x

((((x `) `) `) `) "\/" x = x "\/" (((((x `) `) `) `) "\/" ((x `) `)) by A9

.= x "\/" ((x `) `) by A12 ;

hence ((((x `) `) `) `) "\/" x = x by A5; :: thesis: verum

end;((((x `) `) `) `) "\/" x = x "\/" (((((x `) `) `) `) "\/" ((x `) `)) by A9

.= x "\/" ((x `) `) by A12 ;

hence ((((x `) `) `) `) "\/" x = x by A5; :: thesis: verum

proof

A15:
for x, y being Element of L holds ((x `) `) "\/" ((y "\/" (x `)) `) = (x `) `
let x be Element of L; :: thesis: ((x `) `) ` = x `

((x `) `) ` = (((x `) `) `) "\/" ((((((x `) `) `) `) "\/" x) `) by A8

.= (((x `) `) `) "\/" (x `) by A13 ;

hence ((x `) `) ` = x ` by A12; :: thesis: verum

end;((x `) `) ` = (((x `) `) `) "\/" ((((((x `) `) `) `) "\/" x) `) by A8

.= (((x `) `) `) "\/" (x `) by A13 ;

hence ((x `) `) ` = x ` by A12; :: thesis: verum

proof

A16:
for x being Element of L holds ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) = x
let x, y be Element of L; :: thesis: ((x `) `) "\/" ((y "\/" (x `)) `) = (x `) `

(x `) ` = ((x `) `) "\/" ((y "\/" (((x `) `) `)) `) by A10;

hence ((x `) `) "\/" ((y "\/" (x `)) `) = (x `) ` by A14; :: thesis: verum

end;(x `) ` = ((x `) `) "\/" ((y "\/" (((x `) `) `)) `) by A10;

hence ((x `) `) "\/" ((y "\/" (x `)) `) = (x `) ` by A14; :: thesis: verum

proof

A17:
for x being Element of L holds (x `) ` = x
let x be Element of L; :: thesis: ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) = x

x = ((((x `) `) `) `) "\/" x by A13

.= ((((x `) `) `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" ((((((x `) `) `) `) "\/" x) `)) `) by A7

.= ((((x `) `) `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" (x `)) `) by A13

.= ((x `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" (x `)) `) by A14

.= ((x `) `) "\/" ((((((x `) `) `) `) "\/" (x `)) `) by A14 ;

hence ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) = x by A14; :: thesis: verum

end;x = ((((x `) `) `) `) "\/" x by A13

.= ((((x `) `) `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" ((((((x `) `) `) `) "\/" x) `)) `) by A7

.= ((((x `) `) `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" (x `)) `) by A13

.= ((x `) `) "\/" ((((((((x `) `) `) `) `) `) "\/" (x `)) `) by A14

.= ((x `) `) "\/" ((((((x `) `) `) `) "\/" (x `)) `) by A14 ;

hence ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) = x by A14; :: thesis: verum

proof

A18:
L is join-absorbing
let x be Element of L; :: thesis: (x `) ` = x

thus x = ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) by A16

.= (x `) ` by A15 ; :: thesis: verum

end;thus x = ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) by A16

.= (x `) ` by A15 ; :: thesis: verum

proof

L is meet-Associative
let a, b be Element of L; :: according to LATTICES:def 9 :: thesis: a "/\" (a "\/" b) = a

a "/\" (a "\/" b) = ((a `) "\/" ((a "\/" b) `)) ` by A3

.= ((a `) "\/" ((((a `) `) "\/" b) `)) ` by A17

.= (a `) ` by A8

.= a by A17 ;

hence a "/\" (a "\/" b) = a ; :: thesis: verum

end;a "/\" (a "\/" b) = ((a `) "\/" ((a "\/" b) `)) ` by A3

.= ((a `) "\/" ((((a `) `) "\/" b) `)) ` by A17

.= (a `) ` by A8

.= a by A17 ;

hence a "/\" (a "\/" b) = a ; :: thesis: verum

proof

then reconsider L9 = L as non empty Lattice-like OrthoLattStr by A1, A2, A18;
let a, b, c be Element of L; :: according to ROBBINS3:def 2 :: thesis: a "/\" (b "/\" c) = b "/\" (a "/\" c)

thus a "/\" (b "/\" c) = a "/\" (((b `) "\/" (c `)) `) by A3

.= ((a `) "\/" ((((b `) "\/" (c `)) `) `)) ` by A3

.= ((a `) "\/" ((b `) "\/" (c `))) ` by A17

.= ((b `) "\/" ((a `) "\/" (c `))) ` by A1

.= ((b `) "\/" ((((a `) "\/" (c `)) `) `)) ` by A17

.= ((b `) "\/" ((a "/\" c) `)) ` by A3

.= b "/\" (a "/\" c) by A3 ; :: thesis: verum

end;thus a "/\" (b "/\" c) = a "/\" (((b `) "\/" (c `)) `) by A3

.= ((a `) "\/" ((((b `) "\/" (c `)) `) `)) ` by A3

.= ((a `) "\/" ((b `) "\/" (c `))) ` by A17

.= ((b `) "\/" ((a `) "\/" (c `))) ` by A1

.= ((b `) "\/" ((((a `) "\/" (c `)) `) `)) ` by A17

.= ((b `) "\/" ((a "/\" c) `)) ` by A3

.= b "/\" (a "/\" c) by A3 ; :: thesis: verum

reconsider L9 = L9 as non empty Lattice-like de_Morgan join-Associative meet-Absorbing Orthomodular OrthoLattStr by A3, A6;

L9 is with_Top ;

hence L is Orthomodular_Lattice by A17, ROBBINS3:def 6; :: thesis: verum