let n be Nat; :: thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
let A1 be SetSequence of X; :: thesis: A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
A \ ((superior_setsequence A1) . n) = A \ (Union (A1 ^\ n)) by Th2;
then A \ ((superior_setsequence A1) . n) c= Union (A (\) (A1 ^\ n)) by Th40;
then A \ ((superior_setsequence A1) . n) c= Union ((A (\) A1) ^\ n) by Th18;
hence A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n by Th2; :: thesis: verum