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

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

end;

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