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 Lemsup01;
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 ThChain1;
set q1 = sup M1;
set a = sup L;
set M = F -image (sup L);
A2: f . (sup L) = sup (F -image (sup L)) by Defsupfunc;
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
B1: ( 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
B2: ( g in F & q0 = g . (sup L) ) by B1;
reconsider M2 = g .: L as non empty Chain of Q by ThChain1;
B3: q = sup M2 by Thcontinuous01, B1, B2;
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 set such that
C1: ( x in dom g & x in L & q2 = g . x ) by FUNCT_1:def 12;
reconsider x = x as Element of P by C1;
set Mx = F -image x;
C2: f . x = sup (F -image x) by Defsupfunc;
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 C1, FUNCT_1:def 12;
then C3: f . x <= sup M1 by Lem201;
q2 in F -image x by C1, B2;
then q2 <= sup (F -image x) by Lem201;
hence q2 <= sup M1 by C3, ORDERS_2:26, C2; :: thesis: verum

end;

hence q <= sup M1 by B3, Lem202; :: thesis: verum

end;

hence f . (sup L) <= sup (f .: L) by A2, Lem202; :: thesis: verum

end;

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