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

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