let A be non empty set ; :: thesis: for B being set
for X being Subset of A
for R being Relation of A,B holds { (R .: x) where x is Element of A : x in X } is Subset-Family of B
let B be set ; :: thesis: for X being Subset of A
for R being Relation of A,B holds { (R .: x) where x is Element of A : x in X } is Subset-Family of B
let X be Subset of A; :: thesis: for R being Relation of A,B holds { (R .: x) where x is Element of A : x in X } is Subset-Family of B
let R be Relation of A,B; :: thesis: { (R .: x) where x is Element of A : x in X } is Subset-Family of B
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 B from DOMAIN_1:sch 8(); :: thesis: verum