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

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