let L be complete LATTICE; :: thesis: for S being closure System of L holds Image () = RelStr(# the carrier of S, the InternalRel of S #)
let S be non empty full infs-inheriting SubRelStr of L; :: thesis: Image () = RelStr(# the carrier of S, the InternalRel of S #)
the carrier of (Image ()) = 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 ())
let x be object ; :: thesis: ( x in the carrier of (Image ()) implies x in the carrier of S )
assume x in the carrier of (Image ()) ; :: thesis: x in the carrier of S
then reconsider a = x as Element of (Image ()) ;
consider b being Element of L such that
A1: a = () . b by YELLOW_2:10;
set X = () /\ the carrier of S;
reconsider X = () /\ 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 ;
hence x in the carrier of S by ; :: 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 ()) )
assume x in the carrier of S ; :: thesis: x in the carrier of (Image ())
then reconsider a = x as Element of S ;
reconsider a = a as Element of L by YELLOW_0:58;
set X = () /\ the carrier of S;
A3: (id L) . a = a ;
a <= a ;
then a in uparrow a by WAYBEL_0:18;
then A4: a in () /\ the carrier of S by XBOOLE_0:def 4;
(closure_op S) . a = "/\" ((() /\ the carrier of S),L) by Def5;
then A5: (closure_op S) . a <= a by ;
id L <= closure_op S by WAYBEL_1:def 14;
then a <= () . a by ;
then A6: a = () . a by ;
dom () = the carrier of L by FUNCT_2:def 1;
then a in rng () by ;
hence x in the carrier of (Image ()) by YELLOW_0:def 15; :: thesis: verum
end;
hence Image () = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_0:57; :: thesis: verum