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 Lm21;
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 A1: x in F ; :: thesis: x <= f
then consider g1 being continuous Function of P,Q such that
A2: x = g1 by Lm22;
reconsider g = g1 as Element of (ConPoset (P,Q)) by A2;
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 A3: ( q1 = g1 . p & q2 = (sup_func F) . p ) ; :: thesis: q1 <= q2
then A4: q1 in F -image p by A1, A2;
reconsider M = F -image p as non empty Chain of Q ;
q2 = sup M by Def10, A3;
hence q1 <= q2 by A4, Lm18; :: thesis: verum
end;
hence g1 . p <= (sup_func F) . p ; :: thesis: verum
end;
then g1 <= sup_func F by YELLOW_2:9;
then [g,f] in ConRelat (P,Q) by Def7;
hence x <= f by A2, ORDERS_2:def 5; :: thesis: verum
end;
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)); :: 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
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 ; :: 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 A9: ( 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
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; :: thesis: verum
end;
then sup M <= q2 by Lm19;
hence q1 <= q2 by A9, Def10; :: thesis: verum
end;
hence (sup_func F) . p <= gy . p ; :: thesis: 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; :: 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 A5, YELLOW_0:30; :: thesis: verum