let L be non empty Lattice-like de_Morgan join-Associative meet-Absorbing orthomodular OrthoLattStr ; :: thesis: L is with_Top
deffunc H₁( Element of L) -> Element of the carrier of L = c₁ ` ;
for x, y being Element of L holds x "\/" H₁(x) = y "\/" H₁(y)

proof

A1: for v0, v1 being Element of L holds v0 "\/" H₁(H₁(v0) "\/" H₁(v1)) = v0

proof

let v0, v1 be Element of L; :: thesis: v0 "\/" H₁(H₁(v0) "\/" H₁(v1)) = v0
v0 "/\" v1 = H₁(H₁(v0) "\/" H₁(v1)) by ROBBINS1:def 23;
hence v0 "\/" H₁(H₁(v0) "\/" H₁(v1)) = v0 by ROBBINS3:def 3; :: thesis: verum

end;

A2: for v64 being Element of L holds v64 "\/" H₁(H₁(v64)) = v64

proof

let v64 be Element of L; :: thesis: v64 "\/" H₁(H₁(v64)) = v64

now :: thesis: for v64, v1 being Element of L holds v64 "\/" H₁(H₁(v64)) = v64

let v64, v1 be Element of L; :: thesis: v64 "\/" H₁(H₁(v64)) = v64
H₁(v64) "\/" H₁(H₁(H₁(v64)) "\/" H₁(v1)) = H₁(v64) by A1;
hence v64 "\/" H₁(H₁(v64)) = v64 by A1; :: thesis: verum

end;

hence v64 "\/" H₁(H₁(v64)) = v64 ; :: thesis: verum

end;

A3: for v0, v1 being Element of L holds v0 "\/" H₁(H₁(H₁(v0)) "\/" H₁(v0 "\/" v1)) = v0 "\/" v1

proof

let v0, v1 be Element of L; :: thesis: v0 "\/" H₁(H₁(H₁(v0)) "\/" H₁(v0 "\/" v1)) = v0 "\/" v1
H₁(v0) "/\" (v0 "\/" v1) = H₁(H₁(H₁(v0)) "\/" H₁(v0 "\/" v1)) by ROBBINS1:def 23;
hence v0 "\/" H₁(H₁(H₁(v0)) "\/" H₁(v0 "\/" v1)) = v0 "\/" v1 by Def2; :: thesis: verum

end;

A4: for v1, v64 being Element of L holds v64 "\/" H₁(H₁(v64) "\/" v1) = v64

proof

let v1, v64 be Element of L; :: thesis: v64 "\/" H₁(H₁(v64) "\/" v1) = v64
H₁(v64) "\/" H₁(H₁(H₁(H₁(v64))) "\/" H₁(H₁(v64) "\/" v1)) = H₁(v64) "\/" v1 by A3;
hence v64 "\/" H₁(H₁(v64) "\/" v1) = v64 by A1; :: thesis: verum

end;

A5: for v1, v64, v65 being Element of L holds v64 "\/" v65 = v65 "\/" (v64 "\/" H₁(H₁(v65) "\/" v1))

proof

let v1, v64, v65 be Element of L; :: thesis: v64 "\/" v65 = v65 "\/" (v64 "\/" H₁(H₁(v65) "\/" v1))
v65 "\/" H₁(H₁(v65) "\/" v1) = v65 by A4;
hence v64 "\/" v65 = v65 "\/" (v64 "\/" H₁(H₁(v65) "\/" v1)) by ROBBINS3:def 1; :: thesis: verum

end;

A6: for v64, v65 being Element of L holds v64 "\/" v65 = v65 "\/" (v64 "\/" H₁(H₁(v65)))

proof

let v64, v65 be Element of L; :: thesis: v64 "\/" v65 = v65 "\/" (v64 "\/" H₁(H₁(v65)))
v65 "\/" H₁(H₁(v65)) = v65 by A2;
hence v64 "\/" v65 = v65 "\/" (v64 "\/" H₁(H₁(v65))) by ROBBINS3:def 1; :: thesis: verum

end;

A7: for v64 being Element of L holds v64 "\/" ((v64 `) `) = ((((v64 `) `) `) `) "\/" v64

proof

let v64 be Element of L; :: thesis: v64 "\/" ((v64 `) `) = ((((v64 `) `) `) `) "\/" v64
((((v64 `) `) `) `) "\/" ((v64 `) `) = (v64 `) ` by A2;
hence v64 "\/" ((v64 `) `) = ((((v64 `) `) `) `) "\/" v64 by A6; :: thesis: verum

end;

A8: for v64 being Element of L holds v64 = ((((v64 `) `) `) `) "\/" v64

proof

let v64 be Element of L; :: thesis: v64 = ((((v64 `) `) `) `) "\/" v64
v64 "\/" ((v64 `) `) = v64 by A2;
hence v64 = ((((v64 `) `) `) `) "\/" v64 by A7; :: thesis: verum

end;

A9: for v65 being Element of L holds (((v65 `) `) `) "\/" (v65 `) = ((v65 `) `) `

proof

let v65 be Element of L; :: thesis: (((v65 `) `) `) "\/" (v65 `) = ((v65 `) `) `
((((v65 `) `) `) `) "\/" v65 = v65 by A8;
hence (((v65 `) `) `) "\/" (v65 `) = ((v65 `) `) ` by A4; :: thesis: verum

end;

A10: for v65 being Element of L holds v65 ` = ((v65 `) `) `

proof

let v65 be Element of L; :: thesis: v65 ` = ((v65 `) `) `
(((v65 `) `) `) "\/" (v65 `) = v65 ` by A2;
hence v65 ` = ((v65 `) `) ` by A9; :: thesis: verum

end;

A11: for v65 being Element of L holds H₁(H₁(H₁(H₁(v65)))) "\/" H₁(H₁(H₁(H₁(H₁(H₁(H₁(v65)))))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65

proof

let v65 be Element of L; :: thesis: H₁(H₁(H₁(H₁(v65)))) "\/" H₁(H₁(H₁(H₁(H₁(H₁(H₁(v65)))))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65
H₁(H₁(H₁(H₁(v65)))) "\/" v65 = v65 by A8;
hence H₁(H₁(H₁(H₁(v65)))) "\/" H₁(H₁(H₁(H₁(H₁(H₁(H₁(v65)))))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65 by A3; :: thesis: verum

end;

A12: for v65 being Element of L holds H₁(H₁(v65)) "\/" H₁(H₁(H₁(H₁(H₁(H₁(H₁(v65)))))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65

proof

let v65 be Element of L; :: thesis: H₁(H₁(v65)) "\/" H₁(H₁(H₁(H₁(H₁(H₁(H₁(v65)))))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65
((v65 `) `) ` = v65 ` by A10;
hence H₁(H₁(v65)) "\/" H₁(H₁(H₁(H₁(H₁(H₁(H₁(v65)))))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65 by A11; :: thesis: verum

end;

A13: for v65 being Element of L holds H₁(H₁(v65)) "\/" H₁(H₁(H₁(H₁(H₁(v65)))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65

proof

let v65 be Element of L; :: thesis: H₁(H₁(v65)) "\/" H₁(H₁(H₁(H₁(H₁(v65)))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65
((v65 `) `) ` = v65 ` by A10;
hence H₁(H₁(v65)) "\/" H₁(H₁(H₁(H₁(H₁(v65)))) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65 by A12; :: thesis: verum

end;

A14: for v65 being Element of L holds H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65

proof

let v65 be Element of L; :: thesis: H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65
((v65 `) `) ` = v65 ` by A10;
hence H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = H₁(H₁(H₁(H₁(v65)))) "\/" v65 by A13; :: thesis: verum

end;

A15: for v65 being Element of L holds H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = H₁(H₁(v65)) "\/" v65

proof

let v65 be Element of L; :: thesis: H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = H₁(H₁(v65)) "\/" v65
((v65 `) `) ` = v65 ` by A10;
hence H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = H₁(H₁(v65)) "\/" v65 by A14; :: thesis: verum

end;

A16: for v65 being Element of L holds H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = v65

proof

let v65 be Element of L; :: thesis: H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = v65
((v65 `) `) "\/" v65 = v65 by A2;
hence H₁(H₁(v65)) "\/" H₁(H₁(H₁(v65)) "\/" H₁(v65)) = v65 by A15; :: thesis: verum

end;

A17: for v0, v65 being Element of L holds H₁(H₁(v0)) "\/" H₁(v65 "\/" H₁(v0)) = (v0 `) `

proof

let v0, v65 be Element of L; :: thesis: H₁(H₁(v0)) "\/" H₁(v65 "\/" H₁(v0)) = (v0 `) `
((v0 `) `) ` = v0 ` by A10;
hence H₁(H₁(v0)) "\/" H₁(v65 "\/" H₁(v0)) = (v0 `) ` by A4; :: thesis: verum

end;

A18: for v0 being Element of L holds (v0 `) ` = v0

proof

let v0 be Element of L; :: thesis: (v0 `) ` = v0
H₁(H₁(v0)) "\/" H₁(H₁(H₁(v0)) "\/" H₁(v0)) = (v0 `) ` by A17;
hence (v0 `) ` = v0 by A16; :: thesis: verum

end;

A19: for v1, v64 being Element of L holds v64 "\/" H₁(H₁(H₁(v64)) "\/" H₁(v1 "\/" v64)) = v64 "\/" (v1 "\/" H₁(H₁(v64)))

proof

let v1, v64 be Element of L; :: thesis: v64 "\/" H₁(H₁(H₁(v64)) "\/" H₁(v1 "\/" v64)) = v64 "\/" (v1 "\/" H₁(H₁(v64)))
v64 "\/" (v1 "\/" H₁(H₁(v64))) = v1 "\/" v64 by A6;
hence v64 "\/" H₁(H₁(H₁(v64)) "\/" H₁(v1 "\/" v64)) = v64 "\/" (v1 "\/" H₁(H₁(v64))) by A3; :: thesis: verum

end;

A20: for v1, v64 being Element of L holds v64 "\/" H₁(H₁(H₁(v64)) "\/" H₁(v1 "\/" v64)) = v1 "\/" v64

proof

let v1, v64 be Element of L; :: thesis: v64 "\/" H₁(H₁(H₁(v64)) "\/" H₁(v1 "\/" v64)) = v1 "\/" v64
v64 "\/" (v1 "\/" ((v64 `) `)) = v1 "\/" v64 by A6;
hence v64 "\/" H₁(H₁(H₁(v64)) "\/" H₁(v1 "\/" v64)) = v1 "\/" v64 by A19; :: thesis: verum

end;

A21: for v0, v1 being Element of L holds v0 "\/" H₁(v0 "\/" H₁(v1 "\/" v0)) = v1 "\/" v0

proof

let v0, v1 be Element of L; :: thesis: v0 "\/" H₁(v0 "\/" H₁(v1 "\/" v0)) = v1 "\/" v0
(v0 `) ` = v0 by A18;
hence v0 "\/" H₁(v0 "\/" H₁(v1 "\/" v0)) = v1 "\/" v0 by A20; :: thesis: verum

end;

A22: for v1, v64 being Element of L holds v64 "\/" (v1 "\/" H₁(v64)) = H₁(v64) "\/" v64

proof

let v1, v64 be Element of L; :: thesis: v64 "\/" (v1 "\/" H₁(v64)) = H₁(v64) "\/" v64
H₁(v64) "\/" H₁(H₁(v64) "\/" H₁(v1 "\/" H₁(v64))) = v1 "\/" H₁(v64) by A21;
hence v64 "\/" (v1 "\/" H₁(v64)) = H₁(v64) "\/" v64 by A5; :: thesis: verum

end;

A23: for v0, v65 being Element of L holds H₁(v0) "\/" H₁(v0 "\/" v65) = v0 `

proof

let v0, v65 be Element of L; :: thesis: H₁(v0) "\/" H₁(v0 "\/" v65) = v0 `
(v0 `) ` = v0 by A18;
hence H<sub>1</sub>(v0) "\/" H<sub>1</sub>(v0 "\/" v65) = v0 ` by A4; :: thesis: verum

end;

A24: for v0, v1 being Element of L holds (v0 "\/" v1) "\/" H₁(v0) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1)

proof

let v0, v1 be Element of L; :: thesis: (v0 "\/" v1) "\/" H₁(v0) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1)
(v0 `) "\/" H₁(v0 "\/" v1) = H₁(v0) by A23;
hence (v0 "\/" v1) "\/" H₁(v0) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1) by A22; :: thesis: verum

end;

A25: for v0, v1 being Element of L holds v0 "\/" (v1 "\/" H₁(v0)) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1)

proof

let v0, v1 be Element of L; :: thesis: v0 "\/" (v1 "\/" H₁(v0)) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1)
(v0 "\/" v1) "\/" H₁(v0) = v0 "\/" (v1 "\/" H₁(v0)) by ROBBINS3:def 1;
hence v0 "\/" (v1 "\/" H₁(v0)) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1) by A24; :: thesis: verum

end;

A26: for v0, v1, v65 being Element of L holds v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1)

proof

let v0, v1, v65 be Element of L; :: thesis: v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1)
(v0 "\/" v1) "\/" (v65 "\/" H₁(v0 "\/" v1)) = v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) by ROBBINS3:def 1;
hence v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) = H₁(v0 "\/" v1) "\/" (v0 "\/" v1) by A22; :: thesis: verum

end;

A27: for v0, v1, v65 being Element of L holds v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) = v0 "\/" (v1 "\/" H₁(v0))

proof

let v0, v1, v65 be Element of L; :: thesis: v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) = v0 "\/" (v1 "\/" H₁(v0))
H₁(v0 "\/" v1) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H₁(v0)) by A25;
hence v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) = v0 "\/" (v1 "\/" H₁(v0)) by A26; :: thesis: verum

end;

A28: for v0, v1, v65 being Element of L holds H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1)))

proof

let v0, v1, v65 be Element of L; :: thesis: H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1)))
(v0 "\/" v1) "\/" (v65 "\/" H₁(v0 "\/" v1)) = v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) by ROBBINS3:def 1;
hence H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) by A22; :: thesis: verum

end;

A29: for v0, v1 being Element of L holds H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H₁(v0))

proof

let v0, v1 be Element of L; :: thesis: H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H₁(v0))

now :: thesis: for v65, v1, v0 being Element of L holds H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H₁(v0))

let v65, v1, v0 be Element of L; :: thesis: H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H₁(v0))
v0 "\/" (v1 "\/" (v65 "\/" H₁(v0 "\/" v1))) = v0 "\/" (v1 "\/" H₁(v0)) by A27;
hence H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H₁(v0)) by A28; :: thesis: verum

end;

hence H₁(v1 "\/" v0) "\/" (v0 "\/" v1) = v0 "\/" (v1 "\/" H₁(v0)) ; :: thesis: verum

end;

A30: for v1, v2, v65 being Element of L holds v2 "\/" (v1 "\/" H₁(v2)) = (v1 "\/" v2) "\/" (v65 "\/" H₁(v1 "\/" v2))

proof

let v1, v2, v65 be Element of L; :: thesis: v2 "\/" (v1 "\/" H₁(v2)) = (v1 "\/" v2) "\/" (v65 "\/" H₁(v1 "\/" v2))
H₁(v1 "\/" v2) "\/" (v2 "\/" v1) = v2 "\/" (v1 "\/" H₁(v2)) by A29;
hence v2 "\/" (v1 "\/" H₁(v2)) = (v1 "\/" v2) "\/" (v65 "\/" H₁(v1 "\/" v2)) by A22; :: thesis: verum

end;

A31: for v1, v2, v65 being Element of L holds v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v65 "\/" H₁(v1 "\/" v2)))

proof

let v1, v2, v65 be Element of L; :: thesis: v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v65 "\/" H<sub>1</sub>(v1 "\/" v2)))
(v1 "\/" v2) "\/" (v65 "\/" H<sub>1</sub>(v1 "\/" v2)) = v1 "\/" (v2 "\/" (v65 "\/" H<sub>1</sub>(v1 "\/" v2))) by ROBBINS3:def 1;
hence v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v65 "\/" H₁(v1 "\/" v2))) by A30; :: thesis: verum

end;

A32: for v1, v2 being Element of L holds v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v1 `))

proof

let v1, v2 be Element of L; :: thesis: v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v1 `))

now :: thesis: for v65, v2, v1 being Element of L holds v2 "\/" (v1 "\/" H₁(v2)) = v1 "\/" (v2 "\/" H₁(v1))

let v65, v2, v1 be Element of L; :: thesis: v2 "\/" (v1 "\/" H₁(v2)) = v1 "\/" (v2 "\/" H₁(v1))
v1 "\/" (v2 "\/" (v65 "\/" H₁(v1 "\/" v2))) = v1 "\/" (v2 "\/" H₁(v1)) by A27;
hence v2 "\/" (v1 "\/" H₁(v2)) = v1 "\/" (v2 "\/" H₁(v1)) by A31; :: thesis: verum

end;

hence v2 "\/" (v1 "\/" (v2 `)) = v1 "\/" (v2 "\/" (v1 `)) ; :: thesis: verum

end;

A33: for v0, v1 being Element of L holds v0 "\/" (v0 `) = v1 "\/" (v0 "\/" (v1 `))

proof

let v0, v1 be Element of L; :: thesis: v0 "\/" (v0 `) = v1 "\/" (v0 "\/" (v1 `))
v0 "\/" (v1 "\/" (v0 `)) = v0 "\/" (v0 `) by A22;
hence v0 "\/" (v0 `) = v1 "\/" (v0 "\/" (v1 `)) by A32; :: thesis: verum

end;

let v1, v0 be Element of L; :: thesis: v1 "\/" H₁(v1) = v0 "\/" H₁(v0)
v1 "\/" (v0 "\/" (v1 `)) = v1 "\/" (v1 `) by A22;
hence v1 "\/" H₁(v1) = v0 "\/" H₁(v0) by A33; :: thesis: verum

end;

hence L is with_Top ; :: thesis: verum