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