let L be non empty up-complete Poset; :: thesis: SupMap L is monotone
set P = InclPoset (Ids L);
set f = SupMap L;
for x, y being Element of (InclPoset (Ids L)) st x <= y holds
for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds
a <= b

proof

let x, y be Element of (InclPoset (Ids L)); :: thesis: ( x <= y implies for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds
a <= b )
assume A1: x <= y ; :: thesis: for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds
a <= b
reconsider I = x, J = y as Ideal of L by Th41;
A2: I c= J by A1, YELLOW_1:3;
A3: ( ex_sup_of I,L & ex_sup_of J,L ) by WAYBEL_0:75;
A4: ( (SupMap L) . x = sup I & (SupMap L) . y = sup J ) by Def3;
let a, b be Element of L; :: thesis: ( a = (SupMap L) . x & b = (SupMap L) . y implies a <= b )
assume ( a = (SupMap L) . x & b = (SupMap L) . y ) ; :: thesis: a <= b
hence a <= b by A3, A2, A4, YELLOW_0:34; :: thesis: verum

end;

hence SupMap L is monotone ; :: thesis: verum