let X be set ; :: thesis: for B being SetSequence of X

for n being Nat st B is V55() holds

(inferior_setsequence B) . n = Intersection B

let B be SetSequence of X; :: thesis: for n being Nat st B is V55() holds

(inferior_setsequence B) . n = Intersection B

let n be Nat; :: thesis: ( B is V55() implies (inferior_setsequence B) . n = Intersection B )

defpred S_{1}[ Nat] means (inferior_setsequence B) . $1 = Intersection B;

assume B is V55() ; :: thesis: (inferior_setsequence B) . n = Intersection B

then A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
by Th51;

A2: S_{1}[ 0 ]
by Th17;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A2, A1);

hence (inferior_setsequence B) . n = Intersection B ; :: thesis: verum

for n being Nat st B is V55() holds

(inferior_setsequence B) . n = Intersection B

let B be SetSequence of X; :: thesis: for n being Nat st B is V55() holds

(inferior_setsequence B) . n = Intersection B

let n be Nat; :: thesis: ( B is V55() implies (inferior_setsequence B) . n = Intersection B )

defpred S

assume B is V55() ; :: thesis: (inferior_setsequence B) . n = Intersection B

then A1: for k being Nat st S

S

A2: S

for k being Nat holds S

hence (inferior_setsequence B) . n = Intersection B ; :: thesis: verum