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 object ; :: 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:10;
set X = (uparrow b) /\ the carrier of S;
reconsider X = (uparrow b) /\ the carrier of S as Subset of S by XBOOLE_1:17;
A2: ex_inf_of X,L by YELLOW_0:17;
a = "/\" (X,L) by A1, Def5;
hence x in the carrier of S by A2, YELLOW_0:def 18; :: thesis: verum

end;

set c = closure_op S;
let x be object ; :: 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:58;
set X = (uparrow a) /\ the carrier of S;
A3: (id L) . a = a ;
a <= a ;
then a in uparrow a by WAYBEL_0:18;
then A4: a in (uparrow a) /\ the carrier of S by XBOOLE_0:def 4;
(closure_op S) . a = "/\" (((uparrow a) /\ the carrier of S),L) by Def5;
then A5: (closure_op S) . a <= a by A4, YELLOW_2:22;
id L <= closure_op S by WAYBEL_1:def 14;
then a <= (closure_op S) . a by A3, YELLOW_2:9;
then A6: a = (closure_op S) . a by A5, ORDERS_2:2;
dom (closure_op S) = the carrier of L by FUNCT_2:def 1;
then a in rng (closure_op S) by A6, FUNCT_1:def 3;
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:57; :: thesis: verum