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:21
.= (((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 ` ) by LATTICES:17
.= y |_| (y ` ) by Def7 ;
then b [= y |_| (y ` ) by LATTICES:def 3;
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 ` ) by LATTICES:18
.= y |^| (y ` ) by A7 ;
then y |^| (y ` ) [= b by LATTICES:21;
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 32;
then f OrthoComplement_on L9 by A3, OPOSET_1:def 36;
hence ( L is Orthocomplemented & L is PartialOrdered ) by OPOSET_1:def 37; :: thesis: verum