defpred S1[ set ] means ex x being object st ( x in X & $1 ={x} ); consider F being Subset-Family of X such that A1:
for A being Subset of X holds ( A in F iff S1[A] )
fromSUBSET_1:sch 3(); A2:
for A being Subset of X st A in F holds ( A <>{} & ( for B being Subset of X holds ( not B in F or A = B or A misses B ) ) )