for X being set
for Si being SigmaField of X
for XSeq, YSeq being SetSequence of Si st YSeq = Partial_Intersection XSeq holds
( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) /\ (XSeq . (n + 1)) ) ) by Def1;