let L be non empty OrthoLattRelStr ; :: thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated implies ( L is Orthocomplemented & L is PartialOrdered ) )
assume ( L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated ) ; :: thesis: ( L is Orthocomplemented & L is PartialOrdered )
then reconsider L9 = L as non empty Lattice-like de_Morgan involutive with_Top naturally_sup-generated OrthoLattRelStr ;
reconsider f = the Compl of L9 as Function of L9,L9 ;
for x, y being Element of L9 st x <= y holds
f . x >= f . y

proof

let x, y be Element of L9; :: thesis: ( x <= y implies f . x >= f . y )
assume x <= y ; :: thesis: f . x >= f . y
then x [= y by Th22;
then A1: x ` = (x |^| y) ` by LATTICES:4
.= (((x `) |_| (y `)) `) ` by ROBBINS1:def 23
.= (x `) |_| (y `) by Def6 ;
( f . x = x ` & f . y = y ` ) by ROBBINS1:def 3;
hence f . x >= f . y by A1, Def10; :: thesis: verum

end;

then A2: f is antitone by WAYBEL_9:def 1;
A3: for y being Element of L9 holds
( ex_sup_of {y,(f . y)},L9 & ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )

proof

set xx = "\/" ( the carrier of L9,L9);
let y be Element of L9; :: thesis: ( ex_sup_of {y,(f . y)},L9 & ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
thus ex_sup_of {y,(f . y)},L9 by YELLOW_0:20; :: thesis: ( ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
thus ex_inf_of {y,(f . y)},L9 by YELLOW_0:21; :: thesis: ( "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
set t = y |_| (y `);
for b being Element of L9 st b in the carrier of L9 holds
b <= y |_| (y `)

proof

let b be Element of L9; :: thesis: ( b in the carrier of L9 implies b <= y |_| (y `) )
assume b in the carrier of L9 ; :: thesis: b <= y |_| (y `)
b |_| (y |_| (y `)) = b |_| (b |_| (b `)) by Def7
.= (b |_| b) |_| (b `) by LATTICES:def 5
.= b |_| (b `)
.= y |_| (y `) by Def7 ;
then b [= y |_| (y `) ;
hence b <= y |_| (y `) by Th22; :: thesis: verum

end;

then A4: y |_| (y `) is_>=_than the carrier of L9 by LATTICE3:def 9;
then L9 is upper-bounded by YELLOW_0:def 5;
then A5: ex_sup_of the carrier of L9,L9 by YELLOW_0:43;
reconsider t = y |_| (y `) as Element of L9 ;
A6: for a being Element of L9 st the carrier of L9 is_<=_than a holds
t <= a by LATTICE3:def 9;
"\/" ({y,(f . y)},L9) = "\/" ({y,(y `)},L9) by ROBBINS1:def 3
.= y "|_|" (y `) by YELLOW_0:41
.= y |_| (y `) by Th25
.= "\/" ( the carrier of L9,L9) by A4, A5, A6, YELLOW_0:def 9 ;
hence "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 by A5, WAYBEL_1:def 7; :: thesis: "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9
set xx = "/\" ( the carrier of L9,L9);
set t = y |^| (y `);
A7: for a, b being Element of L9 holds a |^| (a `) = b |^| (b `)

proof

let a, b be Element of L9; :: thesis: a |^| (a `) = b |^| (b `)
a |^| (a `) = ((a `) |_| ((a `) `)) ` by ROBBINS1:def 23
.= ((b `) |_| ((b `) `)) ` by Def7
.= b |^| (b `) by ROBBINS1:def 23 ;
hence a |^| (a `) = b |^| (b `) ; :: thesis: verum

end;

for b being Element of L9 st b in the carrier of L9 holds
b >= y |^| (y `)

proof

let b be Element of L9; :: thesis: ( b in the carrier of L9 implies b >= y |^| (y `) )
assume b in the carrier of L9 ; :: thesis: b >= y |^| (y `)
b |^| (y |^| (y `)) = b |^| (b |^| (b `)) by A7
.= (b |^| b) |^| (b `) by LATTICES:def 7
.= b |^| (b `)
.= y |^| (y `) by A7 ;
then y |^| (y `) [= b by LATTICES:4;
hence b >= y |^| (y `) by Th22; :: thesis: verum

end;

then A8: y |^| (y `) is_<=_than the carrier of L9 by LATTICE3:def 8;
then L9 is lower-bounded by YELLOW_0:def 4;
then A9: ex_inf_of the carrier of L9,L9 by YELLOW_0:42;
reconsider t = y |^| (y `) as Element of L9 ;
A10: for a being Element of L9 st the carrier of L9 is_>=_than a holds
t >= a by LATTICE3:def 8;
"/\" ({y,(f . y)},L9) = "/\" ({y,(y `)},L9) by ROBBINS1:def 3
.= y "|^|" (y `) by YELLOW_0:40
.= y |^| (y `) by Th26
.= "/\" ( the carrier of L9,L9) by A8, A9, A10, YELLOW_0:def 10 ;
hence "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 by A9, WAYBEL_1:def 6; :: thesis: verum

end;

for x being Element of L9 holds f . (f . x) = x

proof

let x be Element of L9; :: thesis: f . (f . x) = x
f . (f . x) = f . (x `) by ROBBINS1:def 3
.= (x `) ` by ROBBINS1:def 3
.= x by Def6 ;
hence f . (f . x) = x ; :: thesis: verum

end;

then f is involutive by PARTIT_2:def 3;
then f is Orderinvolutive by A2, OPOSET_1:def 17;
then f OrthoComplement_on L9 by A3, OPOSET_1:def 21;
hence ( L is Orthocomplemented & L is PartialOrdered ) by OPOSET_1:def 22; :: thesis: verum