let L be non empty up-complete Poset; :: thesis: for S being non empty full SubRelStr of L holds supMap S is monotone
let S be non empty full SubRelStr of L; :: thesis: supMap S is monotone
set f = supMap S;

now

let x, y be Element of (InclPoset (Ids S)); :: thesis: ( x <= y implies (supMap S) . x <= (supMap S) . y )
assume A1: x <= y ; :: thesis: (supMap S) . x <= (supMap S) . y
reconsider I = x, J = y as Ideal of S by YELLOW_2:43;
( I is non empty directed Subset of L & J is non empty directed Subset of L ) by YELLOW_2:7;
then A2: ( ex_sup_of I,L & ex_sup_of J,L ) by WAYBEL_0:75;
A3: I c= J by A1, YELLOW_1:3;
( (supMap S) . x = "\/" I,L & (supMap S) . y = "\/" J,L ) by Def10;
hence (supMap S) . x <= (supMap S) . y by A2, A3, YELLOW_0:34; :: thesis: verum

end;

hence supMap S is monotone by WAYBEL_1:def 2; :: thesis: verum