set f = ClImageMap L;
set R = DsupClOpers L;
set g = corestr ((ClImageMap L) | (DsupClOpers L));
per cases
( ( not DsupClOpers L is empty & not Image ((ClImageMap L) | (DsupClOpers L)) is empty ) or DsupClOpers L is empty or Image ((ClImageMap L) | (DsupClOpers L)) is empty )
;
WAYBEL_0:def 38case
( not
DsupClOpers L is
empty & not
Image ((ClImageMap L) | (DsupClOpers L)) is
empty )
;
( corestr ((ClImageMap L) | (DsupClOpers L)) is one-to-one & corestr ((ClImageMap L) | (DsupClOpers L)) is monotone & ex b1 being Element of bool [: the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the carrier of (DsupClOpers L):] st
( b1 = (corestr ((ClImageMap L) | (DsupClOpers L))) " & b1 is monotone ) )
(ClImageMap L) | (DsupClOpers L) is
V7()
by Th7;
hence
(
corestr ((ClImageMap L) | (DsupClOpers L)) is
V7() &
corestr ((ClImageMap L) | (DsupClOpers L)) is
monotone )
by WAYBEL_1:30;
ex b1 being Element of bool [: the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the carrier of (DsupClOpers L):] st
( b1 = (corestr ((ClImageMap L) | (DsupClOpers L))) " & b1 is monotone )consider f9 being
Function of
((ClosureSystems L) opp),
(ClOpers L) such that A1:
f9 = (ClImageMap L) "
and
f9 is
monotone
by WAYBEL_0:def 38;
reconsider h =
f9 | (Image ((ClImageMap L) | (DsupClOpers L))) as
Function of
(Image ((ClImageMap L) | (DsupClOpers L))),
(DsupClOpers L) by A1, Th8;
take
h
;
( h = (corestr ((ClImageMap L) | (DsupClOpers L))) " & h is monotone )thus h =
((ClImageMap L) | (DsupClOpers L)) "
by A1, Th8
.=
(corestr ((ClImageMap L) | (DsupClOpers L))) "
by WAYBEL_1:30
;
h is monotone let x,
y be
Element of
(Image ((ClImageMap L) | (DsupClOpers L)));
WAYBEL_1:def 2 ( not x <= y or h . x <= h . y )reconsider a =
x,
b =
y as
Element of
((ClosureSystems L) opp) by YELLOW_0:58;
reconsider A =
~ a,
B =
~ b as
strict closure System of
L by Th16;
reconsider i =
closure_op A,
j =
closure_op B as
Element of
(ClOpers L) by Th10;
f9 . y = j
by A1, Th21;
then A2:
h . y = j
by Th6;
assume
x <= y
;
h . x <= h . ythen
a <= b
by YELLOW_0:59;
then
~ a >= ~ b
by YELLOW_7:1;
then A3:
B is
SubRelStr of
A
by Th17;
A4:
B = Image (closure_op B)
by Th18;
A = Image (closure_op A)
by Th18;
then
closure_op A <= closure_op B
by A3, A4, Th14;
then A5:
i <= j
by Th12;
f9 . x = i
by A1, Th21;
then
h . x = i
by Th6;
hence
h . x <= h . y
by A2, A5, YELLOW_0:60;
verum end;