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;

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 38end;

:: 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 b_{1} being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st

( b_{1} = (ClImageMap L) " & b_{1} is monotone ) )

( b

thus
ClImageMap L is V7()
; :: thesis: ( ClImageMap L is monotone & ex b_{1} being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st

( b_{1} = (ClImageMap L) " & b_{1} is monotone ) )

thus ClImageMap L is monotone :: thesis: ex b_{1} being Element of bool [: the carrier of ((ClosureSystems L) opp), the carrier of (ClOpers L):] st

( b_{1} = (ClImageMap L) " & b_{1} is monotone )

thus g = (ClImageMap L) " ; :: thesis: g is monotone

thus g is monotone :: thesis: verum

end;( b

thus ClImageMap L is monotone :: thesis: ex b

( b

proof

take
g
; :: thesis: ( g = (ClImageMap L) " & g is monotone )
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;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

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;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

case
( ClOpers L is empty or (ClosureSystems L) opp is empty )
; :: thesis: ( ClOpers L is empty & (ClosureSystems L) opp is empty )

end;

end;