let P, Q be non empty strict chain-complete Poset; :: thesis: for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is continuous
let F be non empty Chain of (ConPoset (P,Q)); :: thesis: sup_func F is continuous
reconsider f = sup_func F as monotone Function of P,Q by Lm17;
for L being non empty Chain of P holds f . (sup L) <= sup (f .: L)

proof

let L be non empty Chain of P; :: thesis: f . (sup L) <= sup (f .: L)
reconsider M1 = f .: L as non empty Chain of Q by Th1;
set q1 = sup M1;
set a = sup L;
set M = F -image (sup L);
A1: f . (sup L) = sup (F -image (sup L)) by Def10;
for q being Element of Q st q in F -image (sup L) holds
q <= sup M1

proof

let q be Element of Q; :: thesis: ( q in F -image (sup L) implies q <= sup M1 )
assume q in F -image (sup L) ; :: thesis: q <= sup M1
then consider q0 being Element of Q such that
A2: ( q = q0 & ex g being continuous Function of P,Q st
( g in F & q0 = g . (sup L) ) ) ;
consider g being continuous Function of P,Q such that
A3: ( g in F & q0 = g . (sup L) ) by A2;
reconsider M2 = g .: L as non empty Chain of Q by Th1;
A4: q = sup M2 by Th6, A2, A3;
for q2 being Element of Q st q2 in M2 holds
q2 <= sup M1

proof

let q2 be Element of Q; :: thesis: ( q2 in M2 implies q2 <= sup M1 )
assume q2 in M2 ; :: thesis: q2 <= sup M1
then consider x being object such that
A5: ( x in dom g & x in L & q2 = g . x ) by FUNCT_1:def 6;
reconsider x = x as Element of P by A5;
set Mx = F -image x;
A6: f . x = sup (F -image x) by Def10;
set y = f . x;
x in the carrier of P ;
then x in dom f by FUNCT_2:def 1;
then f . x in M1 by A5, FUNCT_1:def 6;
then A7: f . x <= sup M1 by Lm18;
q2 in F -image x by A5, A3;
then q2 <= sup (F -image x) by Lm18;
hence q2 <= sup M1 by A7, A6, ORDERS_2:3; :: thesis: verum

end;

hence q <= sup M1 by A4, Lm19; :: thesis: verum

end;

hence f . (sup L) <= sup (f .: L) by A1, Lm19; :: thesis: verum

end;

hence sup_func F is continuous by Th8; :: thesis: verum