defpred S₁[ set , set ] means ex c being closure Function of L,L st
( c = $1 & $2 = Image c );

A1: now :: thesis: for x being Element of (ClOpers L) ex b being Element of the carrier of ((ClosureSystems L) ~) st S₁[x,b]

let x be Element of (ClOpers L); :: thesis: ex b being Element of the carrier of ((ClosureSystems L) ~) st S₁[x,b]
reconsider c = x as closure Function of L,L by Th10;
reconsider a = Image c as Element of (ClosureSystems L) by Th16;
take b = a ~ ; :: thesis: S₁[x,b]
thus S₁[x,b] ; :: thesis: verum

end;

consider f being Function of (ClOpers L),((ClosureSystems L) opp) such that
A2: for x being Element of (ClOpers L) holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for c being closure Function of L,L holds f . c = Image c
let c be closure Function of L,L; :: thesis: f . c = Image c
c is Element of (ClOpers L) by Th10;
then ex c1 being closure Function of L,L st
( c1 = c & f . c = Image c1 ) by A2;
hence f . c = Image c ; :: thesis: verum