set f = ClImageMap L;
set S = ClOpers L;
set T = (ClosureSystems L) opp ;
reconsider g = (ClImageMap L) " as Function of ((ClosureSystems L) opp),(ClOpers L) by Th20;
per cases ( ( not ClOpers L is empty & not (ClosureSystems L) opp is empty ) or ClOpers L is empty or (ClosureSystems L) opp is empty ) ;
:: according to WAYBEL_0:def 38
case ( not ClOpers L is empty & not (ClosureSystems L) opp is empty ) ; :: thesis: ( ClImageMap L is one-to-one & ClImageMap L is monotone & ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st
( b1 = (ClImageMap L) " & b1 is monotone ) )
thus ClImageMap L is V7() ; :: thesis: ( ClImageMap L is monotone & ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st
( b1 = (ClImageMap L) " & b1 is monotone ) )
thus ClImageMap L is monotone :: thesis: ex b1 being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st
( b1 = (ClImageMap L) " & b1 is monotone )
proof
let x, y be Element of (ClOpers L); :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or (ClImageMap L) . x <= (ClImageMap L) . y )
reconsider c = x, d = y as closure Function of L,L by Th10;
A1: (ClImageMap L) . y = Image d by Def4;
assume x <= y ; :: thesis: (ClImageMap L) . x <= (ClImageMap L) . y
then c <= d by Th12;
then A2: Image d is SubRelStr of Image c by Th14;
(ClImageMap L) . x = Image c by Def4;
then ~ ((ClImageMap L) . x) >= ~ ((ClImageMap L) . y) by A2, A1, Th17;
hence (ClImageMap L) . x <= (ClImageMap L) . y by YELLOW_7:1; :: thesis: verum
end;
take g ; :: thesis: ( g = (ClImageMap L) " & g is monotone )
thus g = (ClImageMap L) " ; :: thesis: g is monotone
thus g is monotone :: thesis: verum
proof
let x, y be Element of ((ClosureSystems L) opp); :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or g . x <= g . y )
reconsider A = ~ x, B = ~ y as strict full infs-inheriting SubRelStr of L by Th16;
A3: B = Image (closure_op B) by Th18;
A4: g . A = closure_op A by Th21;
assume x <= y ; :: thesis: g . x <= g . y
then ~ y <= ~ x by YELLOW_7:1;
then A5: B is SubRelStr of A by Th17;
A6: g . B = closure_op B by Th21;
A = Image (closure_op A) by Th18;
then closure_op A <= closure_op B by A5, A3, Th14;
hence g . x <= g . y by A4, A6, Th12; :: thesis: verum
end;
end;
case ( ClOpers L is empty or (ClosureSystems L) opp is empty ) ; :: thesis: ( ClOpers L is empty & (ClosureSystems L) opp is empty )
hence ( ClOpers L is empty & (ClosureSystems L) opp is empty ) ; :: thesis: verum
end;
end;