let A be non empty set ; :: thesis: for B being set
for X being Subset of
for R being Relation of , holds { (R .: x) where x is Element of A : x in X } is Subset-Family of
let B be set ; :: thesis: for X being Subset of
for R being Relation of , holds { (R .: x) where x is Element of A : x in X } is Subset-Family of
let X be Subset of ; :: thesis: for R being Relation of , holds { (R .: x) where x is Element of A : x in X } is Subset-Family of
let R be Relation of ,; :: thesis: { (R .: x) where x is Element of A : x in X } is Subset-Family of
deffunc H₁( Element of A) -> Element of bool B = R .: $1;
defpred S₁[ set ] means $1 in X;
set Y = { H₁(x) where x is Element of A : S₁[x] } ;
thus { H₁(x) where x is Element of A : S₁[x] } is Subset-Family of from DOMAIN_1:sch 8(); :: thesis: verum