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 `)) `)

proof

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;

A5: for x being Element of L holds x = x "\/" ((x `) `)

proof

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;

assume A6: L is Orthomodular ; :: thesis: L is Orthomodular_Lattice
A7: for x, y being Element of L holds x "\/" y = x "\/" ((((x `) `) "\/" ((x "\/" y) `)) `)

proof

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;

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

proof

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;

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

proof

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;

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

proof

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;

A11: for x being Element of L holds (x `) "\/" (x `) = x `

proof

let x be Element of L; :: thesis: (x `) "\/" (x `) = x `
thus x ` = (x `) "\/" ((x "\/" ((x `) `)) `) by A10
.= (x `) "\/" (x `) by A5 ; :: thesis: verum

end;

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

proof

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;

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

proof

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;

A14: for x being Element of L holds ((x `) `) ` = x `

proof

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;

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

proof

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;

A16: for x being Element of L holds ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) = x

proof

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;

A17: for x being Element of L holds (x `) ` = x

proof

let x be Element of L; :: thesis: (x `) ` = x
thus x = ((x `) `) "\/" ((((x `) `) "\/" (x `)) `) by A16
.= (x `) ` by A15 ; :: thesis: verum

end;

A18: L is join-absorbing

proof

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;

L is meet-Associative

proof

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;

then reconsider L9 = L as non empty Lattice-like OrthoLattStr by A1, A2, A18;
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