let L be complete LATTICE; :: thesis: for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S,the InternalRel of S #)
let S be non empty full infs-inheriting SubRelStr of L; :: thesis: Image (closure_op S) = RelStr(# the carrier of S,the InternalRel of S #)
the carrier of (Image (closure_op S)) = the carrier of S

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of S c= the carrier of (Image (closure_op S))

let x be set ; :: thesis: ( x in the carrier of (Image (closure_op S)) implies x in the carrier of S )
assume x in the carrier of (Image (closure_op S)) ; :: thesis: x in the carrier of S
then reconsider a = x as Element of (Image (closure_op S)) ;
consider b being Element of L such that
A1: a = (closure_op S) . b by YELLOW_2:12;
set X = (uparrow b) /\ the carrier of S;
reconsider X = (uparrow b) /\ the carrier of S as Subset of S by XBOOLE_1:17;
( a = "/\" X,L & ex_inf_of X,L ) by A1, Def6, YELLOW_0:17;
hence x in the carrier of S by YELLOW_0:def 18; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of S or x in the carrier of (Image (closure_op S)) )
assume x in the carrier of S ; :: thesis: x in the carrier of (Image (closure_op S))
then reconsider a = x as Element of S ;
reconsider a = a as Element of L by YELLOW_0:59;
set X = (uparrow a) /\ the carrier of S;
set c = closure_op S;
( id L <= closure_op S & (id L) . a = a ) by TMAP_1:91, WAYBEL_1:def 14;
then A2: a <= (closure_op S) . a by YELLOW_2:10;
a <= a ;
then ( a in uparrow a & a in the carrier of S ) by WAYBEL_0:18;
then ( (closure_op S) . a = "/\" ((uparrow a) /\ the carrier of S),L & a in (uparrow a) /\ the carrier of S ) by Def6, XBOOLE_0:def 4;
then (closure_op S) . a <= a by YELLOW_2:24;
then ( a = (closure_op S) . a & dom (closure_op S) = the carrier of L ) by A2, FUNCT_2:def 1, ORDERS_2:25;
then a in rng (closure_op S) by FUNCT_1:def 5;
hence x in the carrier of (Image (closure_op S)) by YELLOW_0:def 15; :: thesis: verum

end;

hence Image (closure_op S) = RelStr(# the carrier of S,the InternalRel of S #) by YELLOW_0:58; :: thesis: verum