let A be non empty set ; :: thesis: for X being Subset of A holds { {x} where x is Element of A : x in X } is Subset-Family of A
let X be Subset of A; :: thesis: { {x} where x is Element of A : x in X } is Subset-Family of A
{ {x} where x is Element of A : x in X } c= bool A

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { {x} where x is Element of A : x in X } or a in bool A )
assume a in { {x} where x is Element of A : x in X } ; :: thesis: a in bool A
then ex x being Element of A st
( a = {x} & x in X ) ;
then a c= A by ZFMISC_1:31;
hence a in bool A ; :: thesis: verum

end;

hence { {x} where x is Element of A : x in X } is Subset-Family of A ; :: thesis: verum