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