let X be set ; :: thesis: for S being Subset-Family of X
for A being Subset of S holds A is Subset-Family of X
let S be Subset-Family of X; :: thesis: for A being Subset of S holds A is Subset-Family of X
let A be Subset of S; :: thesis: A is Subset-Family of X
S c= bool X ;
then A c= bool X ;
hence A is Subset-Family of X ; :: thesis: verum