let n be Element of 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 7;
hence Intersection B c= (inferior_setsequence B) . n by Th17; :: thesis: verum