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;

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

hence
idsMap S is monotone
by WAYBEL_1:def 2; :: thesis: verum(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;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