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 monotone
let F be non empty Chain of (ConPoset P,Q); :: thesis: sup_func F is monotone
reconsider f = sup_func F as Function of P,Q ;
for p, p1 being Element of P st p <= p1 holds
for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1

proof

let p, p1 be Element of P; :: thesis: ( p <= p1 implies for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1 )
assume A1: p <= p1 ; :: thesis: for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1
for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1

proof

let q, q1 be Element of Q; :: thesis: ( q = f . p & q1 = f . p1 implies q <= q1 )
assume A2: ( q = f . p & q1 = f . p1 ) ; :: thesis: q <= q1
reconsider X = F -image p as non empty Chain of Q ;
reconsider X1 = F -image p1 as non empty Chain of Q ;
A00: ( ex_sup_of X,Q & ex_sup_of X1,Q ) by DefchainComplete;
A3: q = sup X by A2, Defsupfunc;
q1 = sup X1 by A2, Defsupfunc;
then A4: X1 is_<=_than q1 by A00, YELLOW_0:def 9;
for x being Element of Q st x in X holds
x <= q1

proof

let x be Element of Q; :: thesis: ( x in X implies x <= q1 )
assume x in X ; :: thesis: x <= q1
then consider a being Element of Q such that
B2: ( x = 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
B3: ( g in F & a = g . p ) by B2;
reconsider b = g . p1 as Element of Q ;
B4: a <= b by A1, B3, ORDERS_3:def 5;
b in X1 by B3;
then b <= q1 by A4, LATTICE3:def 9;
hence x <= q1 by B2, B4, ORDERS_2:26; :: thesis: verum

end;

then X is_<=_than q1 by LATTICE3:def 9;
hence q <= q1 by A00, A3, YELLOW_0:def 9; :: thesis: verum

end;

hence for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1 ; :: thesis: verum

end;

hence sup_func F is monotone by ORDERS_3:def 5; :: thesis: verum