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 ;
A3: ( ex_sup_of X,Q & ex_sup_of X1,Q ) by Def1;
A4: q = sup X by A2, Def10;
q1 = sup X1 by A2, Def10;
then A5: X1 is_<=_than q1 by A3, 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
A6: ( 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
A7: ( g in F & a = g . p ) by A6;
reconsider b = g . p1 as Element of Q ;
A8: a <= b by A1, A7, ORDERS_3:def 5;
b in X1 by A7;
then b <= q1 by A5;
hence x <= q1 by A6, A8, ORDERS_2:3; :: thesis: verum

end;

then X is_<=_than q1 ;
hence q <= q1 by A3, A4, 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