let L be non empty up-complete Poset; for S being non empty full SubRelStr of L holds supMap S is monotone
let S be non empty full SubRelStr of L; supMap S is monotone
set f = supMap S;
now for x, y being Element of (InclPoset (Ids S)) st x <= y holds
(supMap S) . x <= (supMap S) . ylet x,
y be
Element of
(InclPoset (Ids S));
( 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
;
(supMap S) . x <= (supMap S) . ythen 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;
verum end;
hence
supMap S is monotone
by WAYBEL_1:def 2; verum