let n be Nat; :: thesis: for X being set
for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n
let X be set ; :: thesis: for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n
let B be SetSequence of X; :: thesis: Intersection B c= (inferior_setsequence B) . n
0 <= n by NAT_1:2;
then (inferior_setsequence B) . 0 c= (inferior_setsequence B) . n by PROB_1:def 5;
hence Intersection B c= (inferior_setsequence B) . n by Th17; :: thesis: verum