let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds baseMap B is monotone
let B be with_bottom CLbasis of L; :: thesis: baseMap B is monotone
set f = baseMap B;
now :: thesis: for x, y being Element of L st x <= y holds
(baseMap B) . x <= (baseMap B) . y
let x, y be Element of L; :: thesis: ( x <= y implies (baseMap B) . x <= (baseMap B) . y )
assume A1: x <= y ; :: thesis: (baseMap B) . x <= (baseMap B) . y
A2: (baseMap B) . y = (waybelow y) /\ B by Def12;
(baseMap B) . x = (waybelow x) /\ B by Def12;
then (baseMap B) . x c= (baseMap B) . y by A1, A2, WAYBEL_3:12, XBOOLE_1:26;
hence (baseMap B) . x <= (baseMap B) . y by YELLOW_1:3; :: thesis: verum
end;
hence baseMap B is monotone by WAYBEL_1:def 2; :: thesis: verum