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 L' = L as non empty Lattice-like de_Morgan involutive with_Top naturally_sup-generated OrthoLattRelStr ;
reconsider f = the Compl of L' as Function of L',L' ;
for x being Element of L' holds f . (f . x) = x
then A1:
f is dneg
by OPOSET_1:def 3;
for x, y being Element of L' st x <= y holds
f . x >= f . y
then
f is antitone
by WAYBEL_9:def 1;
then A5:
f is Orderinvolutive
by A1, OPOSET_1:def 32;
for y being Element of L' holds
( ex_sup_of {y,(f . y)},L' & ex_inf_of {y,(f . y)},L' & "\/" {y,(f . y)},L' is_maximum_of the carrier of L' & "/\" {y,(f . y)},L' is_minimum_of the carrier of L' )
proof
let y be
Element of
L';
:: thesis: ( ex_sup_of {y,(f . y)},L' & ex_inf_of {y,(f . y)},L' & "\/" {y,(f . y)},L' is_maximum_of the carrier of L' & "/\" {y,(f . y)},L' is_minimum_of the carrier of L' )
thus
ex_sup_of {y,(f . y)},
L'
by YELLOW_0:20;
:: thesis: ( ex_inf_of {y,(f . y)},L' & "\/" {y,(f . y)},L' is_maximum_of the carrier of L' & "/\" {y,(f . y)},L' is_minimum_of the carrier of L' )
thus
ex_inf_of {y,(f . y)},
L'
by YELLOW_0:21;
:: thesis: ( "\/" {y,(f . y)},L' is_maximum_of the carrier of L' & "/\" {y,(f . y)},L' is_minimum_of the carrier of L' )
set t =
y |_| (y ` );
for
b being
Element of
L' st
b in the
carrier of
L' holds
b <= y |_| (y ` )
then A6:
y |_| (y ` ) is_>=_than the
carrier of
L'
by LATTICE3:def 9;
then
L' is
upper-bounded
by YELLOW_0:def 5;
then A7:
ex_sup_of the
carrier of
L',
L'
by YELLOW_0:43;
reconsider t =
y |_| (y ` ) as
Element of
L' ;
set xx =
"\/" the
carrier of
L',
L';
A8:
for
a being
Element of
L' st the
carrier of
L' is_<=_than a holds
t <= a
by LATTICE3:def 9;
"\/" {y,(f . y)},
L' =
"\/" {y,(y ` )},
L'
by ROBBINS1:def 3
.=
y "|_|" (y ` )
by YELLOW_0:41
.=
y |_| (y ` )
by Th25
.=
"\/" the
carrier of
L',
L'
by A6, A7, A8, YELLOW_0:def 9
;
hence
"\/" {y,(f . y)},
L' is_maximum_of the
carrier of
L'
by A7, WAYBEL_1:def 7;
:: thesis: "/\" {y,(f . y)},L' is_minimum_of the carrier of L'
A9:
for
a,
b being
Element of
L' holds
a |^| (a ` ) = b |^| (b ` )
set t =
y |^| (y ` );
for
b being
Element of
L' st
b in the
carrier of
L' holds
b >= y |^| (y ` )
then A10:
y |^| (y ` ) is_<=_than the
carrier of
L'
by LATTICE3:def 8;
then
L' is
lower-bounded
by YELLOW_0:def 4;
then A11:
ex_inf_of the
carrier of
L',
L'
by YELLOW_0:42;
reconsider t =
y |^| (y ` ) as
Element of
L' ;
set xx =
"/\" the
carrier of
L',
L';
A12:
for
a being
Element of
L' st the
carrier of
L' is_>=_than a holds
t >= a
by LATTICE3:def 8;
"/\" {y,(f . y)},
L' =
"/\" {y,(y ` )},
L'
by ROBBINS1:def 3
.=
y "|^|" (y ` )
by YELLOW_0:40
.=
y |^| (y ` )
by Th26
.=
"/\" the
carrier of
L',
L'
by A10, A11, A12, YELLOW_0:def 10
;
hence
"/\" {y,(f . y)},
L' is_minimum_of the
carrier of
L'
by A11, WAYBEL_1:def 6;
:: thesis: verum
end;
then
f OrthoComplement_on L'
by A5, OPOSET_1:def 36;
hence
( L is Orthocomplemented & L is PartialOrdered )
by OPOSET_1:def 37; :: thesis: verum