let L be non empty reflexive transitive RelStr ; :: thesis: for S being non empty full SubRelStr of L holds idsMap S is monotone
let S be non empty full SubRelStr of L; :: thesis: idsMap S is monotone
set f = idsMap S;

now

let x, y be Element of (InclPoset (Ids S)); :: thesis: ( x <= y implies (idsMap S) . x <= (idsMap S) . y )
assume A1: x <= y ; :: thesis: (idsMap S) . x <= (idsMap S) . y
reconsider I = x, J = y as Ideal of S by YELLOW_2:43;
consider K1 being Subset of L such that
A2: I = K1 and
A3: (idsMap S) . x = downarrow K1 by Def11;
consider K2 being Subset of L such that
A4: J = K2 and
A5: (idsMap S) . y = downarrow K2 by Def11;
I c= J by A1, YELLOW_1:3;
then downarrow K1 c= downarrow K2 by A2, A4, YELLOW_3:6;
hence (idsMap S) . x <= (idsMap S) . y by A3, A5, YELLOW_1:3; :: thesis: verum

end;

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