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 ) ;
:: according to WAYBEL_0:def 38

case ( not DsupClOpers L is empty & not Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; :: thesis: ( corestr ((ClImageMap L) | (DsupClOpers L)) is one-to-one & corestr ((ClImageMap L) | (DsupClOpers L)) is monotone & ex b₁ being Element of bool [: the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the carrier of (DsupClOpers L):] st
( b₁ = (corestr ((ClImageMap L) | (DsupClOpers L))) " & b₁ is monotone ) )

(ClImageMap L) | (DsupClOpers L) is one-to-one by Th7;
hence ( corestr ((ClImageMap L) | (DsupClOpers L)) is one-to-one & corestr ((ClImageMap L) | (DsupClOpers L)) is monotone ) by WAYBEL_1:30; :: thesis: ex b₁ being Element of bool [: the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the carrier of (DsupClOpers L):] st
( b₁ = (corestr ((ClImageMap L) | (DsupClOpers L))) " & b₁ 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 ; :: thesis: ( 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 ; :: thesis: h is monotone
let x, y be Element of (Image ((ClImageMap L) | (DsupClOpers L))); :: according to WAYBEL_1:def 2 :: thesis: ( 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 ; :: thesis: h . x <= h . y
then 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; :: thesis: verum

end;

case ( DsupClOpers L is empty or Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; :: thesis: ( DsupClOpers L is empty & Image ((ClImageMap L) | (DsupClOpers L)) is empty )

hence ( DsupClOpers L is empty & Image ((ClImageMap L) | (DsupClOpers L)) is empty ) ; :: thesis: verum

end;

end;