for X, x being set
for R being Subset-Family of X st x in X holds
( x in Intersect R iff for Y being set st Y in R holds
x in Y )