let X be set ; :: thesis: for R being Relation of X holds <.(rho R).] = rho R
let R be Relation of X; :: thesis: <.(rho R).] = rho R
<.(rho R).] c= rho R

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in <.(rho R).] or t in rho R )
assume A1: t in <.(rho R).] ; :: thesis: t in rho R
then reconsider u = t as Subset of [:X,X:] ;
consider b being Element of rho R such that
A2: b c= u by A1, CARDFIL2:def 8;
b in rho R ;
then ex c being Subset of [:X,X:] st
( b = c & R c= c ) ;
then R c= u by A2;
hence t in rho R ; :: thesis: verum

end;

hence <.(rho R).] = rho R by CARDFIL2:18; :: thesis: verum