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 :: thesis: for x, y being Element of (InclPoset (Ids S)) st x <= y holds
(supMap S) . x <= (supMap S) . y

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

end;

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