let X be set ; :: thesis: for SF being Subset-Family of [:X,X:]
for R being Relation of X st SF = rho R holds
SF c= rho (meet SF)
let SF be Subset-Family of [:X,X:]; :: thesis: for R being Relation of X st SF = rho R holds
SF c= rho (meet SF)
let R be Relation of X; :: thesis: ( SF = rho R implies SF c= rho (meet SF) )
assume A1: SF = rho R ; :: thesis: SF c= rho (meet SF)
SF c= rho (meet SF)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SF or x in rho (meet SF) )
assume A2: x in SF ; :: thesis: x in rho (meet SF)
then consider S being Subset of [:X,X:] such that
A3: x = S and
R c= S by A1;
meet SF c= S by A3, A2, SETFAM_1:def 1;
hence x in rho (meet SF) by A3; :: thesis: verum

end;

hence SF c= rho (meet SF) ; :: thesis: verum