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