let X be set ; :: thesis: for R being Relation of X holds <.{R}.] = rho R
let R be Relation of X; :: thesis: <.{R}.] = rho R
thus <.{R}.] c= rho R :: according to XBOOLE_0:def 10 :: thesis: rho R c= <.{R}.]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <.{R}.] or x in rho R )
assume A2: x in <.{R}.] ; :: thesis: x in rho R
then reconsider y = x as Subset of [:X,X:] ;
consider b being Element of {R} such that
A3: b c= y by A2, CARDFIL2:def 8;
R c= y by A3, TARSKI:def 1;
hence x in rho R ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rho R or x in <.{R}.] )
assume x in rho R ; :: thesis: x in <.{R}.]
then consider S being Relation of X such that
A4: x = S and
A5: R c= S ;
R is Element of {R} by TARSKI:def 1;
hence x in <.{R}.] by A4, A5, CARDFIL2:def 8; :: thesis: verum