let L be non empty up-complete Poset; :: thesis: for S being non empty full SubRelStr of L holds supMap S is monotone

let S be non empty full SubRelStr of L; :: thesis: supMap S is monotone

set f = supMap S;

let S be non empty full SubRelStr of L; :: thesis: supMap S is monotone

set f = supMap S;

now :: thesis: for x, y being Element of (InclPoset (Ids S)) st x <= y holds

(supMap S) . x <= (supMap S) . y

hence
supMap S is monotone
by WAYBEL_1:def 2; :: thesis: verum(supMap S) . x <= (supMap S) . y

let x, y be Element of (InclPoset (Ids S)); :: thesis: ( x <= y implies (supMap S) . x <= (supMap S) . y )

reconsider I = x, J = y as Ideal of S by YELLOW_2:41;

assume x <= y ; :: thesis: (supMap S) . x <= (supMap S) . y

then A1: I c= J by YELLOW_1:3;

I is non empty directed Subset of L by YELLOW_2:7;

then A2: ex_sup_of I,L by WAYBEL_0:75;

J is non empty directed Subset of L by YELLOW_2:7;

then A3: ex_sup_of J,L by WAYBEL_0:75;

A4: (supMap S) . y = "\/" (J,L) by Def10;

(supMap S) . x = "\/" (I,L) by Def10;

hence (supMap S) . x <= (supMap S) . y by A2, A3, A1, A4, YELLOW_0:34; :: thesis: verum

end;reconsider I = x, J = y as Ideal of S by YELLOW_2:41;

assume x <= y ; :: thesis: (supMap S) . x <= (supMap S) . y

then A1: I c= J by YELLOW_1:3;

I is non empty directed Subset of L by YELLOW_2:7;

then A2: ex_sup_of I,L by WAYBEL_0:75;

J is non empty directed Subset of L by YELLOW_2:7;

then A3: ex_sup_of J,L by WAYBEL_0:75;

A4: (supMap S) . y = "\/" (J,L) by Def10;

(supMap S) . x = "\/" (I,L) by Def10;

hence (supMap S) . x <= (supMap S) . y by A2, A3, A1, A4, YELLOW_0:34; :: thesis: verum