let P, Q be non empty strict chain-complete Poset; :: thesis: 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)); :: thesis: ( 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 Lemsup03;
for x being Element of (ConPoset (P,Q)) st x in F holds
x <= f

proof

let x be Element of (ConPoset (P,Q)); :: thesis: ( x in F implies x <= f )
assume B1: x in F ; :: thesis: x <= f
then consider g1 being continuous Function of P,Q such that
B2: x = g1 by Lem301;
reconsider g = g1 as Element of (ConPoset (P,Q)) by B2;
for p being Element of P holds g1 . p <= (sup_func F) . p

proof

let p be Element of P; :: thesis: g1 . p <= (sup_func F) . p
for q1, q2 being Element of Q st q1 = g1 . p & q2 = (sup_func F) . p holds
q1 <= q2

proof

let q1, q2 be Element of Q; :: thesis: ( q1 = g1 . p & q2 = (sup_func F) . p implies q1 <= q2 )
assume C1: ( q1 = g1 . p & q2 = (sup_func F) . p ) ; :: thesis: q1 <= q2
then C2: q1 in F -image p by B1, B2;
reconsider M = F -image p as non empty Chain of Q ;
q2 = sup M by Defsupfunc, C1;
hence q1 <= q2 by C2, Lem201; :: thesis: verum

end;

hence g1 . p <= (sup_func F) . p ; :: thesis: verum

end;

then g1 <= sup_func F by YELLOW_2:10;
then [g,f] in ConRelat (P,Q) by DefConRelat;
hence x <= f by B2, ORDERS_2:def 9; :: thesis: verum

end;

then A1: F is_<=_than f by LATTICE3:def 9;
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)); :: thesis: ( 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
B01: ( y = y1 & ex gy being continuous Function of P,Q st gy = y1 ) ;
consider gy being continuous Function of P,Q such that
B02: gy = y1 by B01;
( F is_<=_than y implies f <= y )

proof

assume B1: F is_<=_than y ; :: thesis: f <= y
for p being Element of P holds (sup_func F) . p <= gy . p

proof

let p be Element of P; :: thesis: (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; :: thesis: ( q1 = (sup_func F) . p & q2 = gy . p implies q1 <= q2 )
assume C1: ( q1 = (sup_func F) . p & q2 = gy . p ) ; :: thesis: 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; :: thesis: ( q in M implies q <= q2 )
assume q in M ; :: thesis: q <= q2
then consider a being Element of Q such that
D1: ( 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
D2: ( g in F & a = g . p ) by D1;
reconsider g1 = g as Element of (ConPoset (P,Q)) by D2;
g1 <= y by B1, LATTICE3:def 9, D2;
then [g1,y] in ConRelat (P,Q) by ORDERS_2:def 9;
then consider g2, g3 being Function of P,Q such that
D3: ( g1 = g2 & y = g3 & g2 <= g3 ) by DefConRelat;
thus q <= q2 by D3, B01, B02, D1, D2, C1, YELLOW_2:10; :: thesis: verum

end;

then sup M <= q2 by Lem202;
hence q1 <= q2 by C1, Defsupfunc; :: thesis: verum

end;

hence (sup_func F) . p <= gy . p ; :: thesis: verum

end;

then sup_func F <= gy by YELLOW_2:10;
then [f,y] in ConRelat (P,Q) by B01, B02, DefConRelat;
hence f <= y by ORDERS_2:def 9; :: thesis: verum

end;

hence ( F is_<=_than y implies f <= y ) ; :: thesis: verum

end;

hence ( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) ) by A1, YELLOW_0:30; :: thesis: verum