let n be Nat; :: thesis: for X being set
for B being SetSequence of X holds (superior_setsequence B) . n c= Union B
let X be set ; :: thesis: for B being SetSequence of X holds (superior_setsequence B) . n c= Union B
let B be SetSequence of X; :: thesis: (superior_setsequence B) . n c= Union B
0 <= n by NAT_1:2;
then (superior_setsequence B) . n c= (superior_setsequence B) . 0 by PROB_1:def 4;
hence (superior_setsequence B) . n c= Union B by Th18; :: thesis: verum