let P, Q be non empty strict chain-complete Poset; for F being non empty Chain of (ConPoset (P,Q)) holds
( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )
let F be non empty Chain of (ConPoset (P,Q)); ( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )
set X = ConPoset (P,Q);
set f1 = sup_func F;
reconsider f = sup_func F as Element of (ConPoset (P,Q)) by Lm21;
for x being Element of (ConPoset (P,Q)) st x in F holds
x <= f
then A5:
F is_<=_than f
;
for y being Element of (ConPoset (P,Q)) st F is_<=_than y holds
f <= y
proof
let y be
Element of
(ConPoset (P,Q));
( F is_<=_than y implies f <= y )
y in ConFuncs (
P,
Q)
;
then consider y1 being
Element of
Funcs ( the
carrier of
P, the
carrier of
Q)
such that A6:
(
y = y1 & ex
gy being
continuous Function of
P,
Q st
gy = y1 )
;
consider gy being
continuous Function of
P,
Q such that A7:
gy = y1
by A6;
(
F is_<=_than y implies
f <= y )
proof
assume A8:
F is_<=_than y
;
f <= y
for
p being
Element of
P holds
(sup_func F) . p <= gy . p
proof
let p be
Element of
P;
(sup_func F) . p <= gy . p
for
q1,
q2 being
Element of
Q st
q1 = (sup_func F) . p &
q2 = gy . p holds
q1 <= q2
proof
let q1,
q2 be
Element of
Q;
( q1 = (sup_func F) . p & q2 = gy . p implies q1 <= q2 )
assume A9:
(
q1 = (sup_func F) . p &
q2 = gy . p )
;
q1 <= q2
reconsider M =
F -image p as non
empty Chain of
Q ;
for
q being
Element of
Q st
q in M holds
q <= q2
proof
let q be
Element of
Q;
( q in M implies q <= q2 )
assume
q in M
;
q <= q2
then consider a being
Element of
Q such that A10:
(
q = a & ex
g being
continuous Function of
P,
Q st
(
g in F &
a = g . p ) )
;
consider g being
continuous Function of
P,
Q such that A11:
(
g in F &
a = g . p )
by A10;
reconsider g1 =
g as
Element of
(ConPoset (P,Q)) by A11;
g1 <= y
by A8, A11;
then
[g1,y] in ConRelat (
P,
Q)
by ORDERS_2:def 5;
then consider g2,
g3 being
Function of
P,
Q such that A12:
(
g1 = g2 &
y = g3 &
g2 <= g3 )
by Def7;
thus
q <= q2
by A12, A6, A7, A10, A11, A9, YELLOW_2:9;
verum
end;
then
sup M <= q2
by Lm19;
hence
q1 <= q2
by A9, Def10;
verum
end;
hence
(sup_func F) . p <= gy . p
;
verum
end;
then
sup_func F <= gy
by YELLOW_2:9;
then
[f,y] in ConRelat (
P,
Q)
by A6, A7, Def7;
hence
f <= y
by ORDERS_2:def 5;
verum
end;
hence
(
F is_<=_than y implies
f <= y )
;
verum
end;
hence
( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )
by A5, YELLOW_0:30; verum