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