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;

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

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