now :: thesis: for n being Nat holds (inferior_setsequence S) . n in Si

then
rng (inferior_setsequence S) c= Si
by NAT_1:52;let n be Nat; :: thesis: (inferior_setsequence S) . n in Si

reconsider DSeq = S ^\ n as SetSequence of X ;

reconsider n1 = n as Nat ;

for m being Nat holds DSeq . m in Si

then A1: Intersection DSeq in Si by PROB_1:def 6;

Intersection DSeq = meet (rng DSeq) by Th8;

then Intersection DSeq = meet { (S . k) where k is Nat : n1 <= k } by Th6;

hence (inferior_setsequence S) . n in Si by A1, Def2; :: thesis: verum

end;reconsider DSeq = S ^\ n as SetSequence of X ;

reconsider n1 = n as Nat ;

for m being Nat holds DSeq . m in Si

proof

then
rng DSeq c= Si
by NAT_1:52;
let m be Nat; :: thesis: DSeq . m in Si

( DSeq . m = S . (m + n1) & S . (m + n1) in rng S ) by NAT_1:51, NAT_1:def 3;

hence DSeq . m in Si ; :: thesis: verum

end;( DSeq . m = S . (m + n1) & S . (m + n1) in rng S ) by NAT_1:51, NAT_1:def 3;

hence DSeq . m in Si ; :: thesis: verum

then A1: Intersection DSeq in Si by PROB_1:def 6;

Intersection DSeq = meet (rng DSeq) by Th8;

then Intersection DSeq = meet { (S . k) where k is Nat : n1 <= k } by Th6;

hence (inferior_setsequence S) . n in Si by A1, Def2; :: thesis: verum

hence inferior_setsequence S is SetSequence of Si by RELAT_1:def 19; :: thesis: verum