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, ROBBINS3:def 3
.= x "\/" (((x ` ) "\/" (y ` )) ` ) by A3, ROBBINS1:def 23 ; :: 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, ROBBINS1:def 23
.= x "\/" ((x ` ) ` ) by A2, ROBBINS3:def 3 ; :: 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, Def2
.= x "\/" ((((x ` ) ` ) "\/" ((x "\/" y) ` )) ` ) by A3, ROBBINS1:def 23 ; :: 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, ROBBINS3:def 1; :: 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, ROBBINS1:def 23
.= ((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, ROBBINS1:def 23
.= ((a ` ) "\/" ((((b ` ) "\/" (c ` )) ` ) ` )) ` by A3, ROBBINS1:def 23
.= ((a ` ) "\/" ((b ` ) "\/" (c ` ))) ` by A17
.= ((b ` ) "\/" ((a ` ) "\/" (c ` ))) ` by A1, ROBBINS3:def 1
.= ((b ` ) "\/" ((((a ` ) "\/" (c ` )) ` ) ` )) ` by A17
.= ((b ` ) "\/" ((a "/\" c) ` )) ` by A3, ROBBINS1:def 23
.= b "/\" (a "/\" c) by A3, ROBBINS1:def 23 ; :: 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