let n be Nat; :: thesis: for X, x being set
for A1 being SetSequence of X holds
( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )
let X, x be set ; :: thesis: for A1 being SetSequence of X holds
( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )
let A1 be SetSequence of X; :: thesis: ( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )
thus ( x in (Partial_Intersection A1) . n implies for k being Nat st k <= n holds
x in A1 . k ) :: thesis: ( ( for k being Nat st k <= n holds
x in A1 . k ) implies x in (Partial_Intersection A1) . n )

proof

assume A1: x in (Partial_Intersection A1) . n ; :: thesis: for k being Nat st k <= n holds
x in A1 . k
for k being Nat st k <= n holds
x in A1 . k

proof

let k be Nat; :: thesis: ( k <= n implies x in A1 . k )
assume A2: k <= n ; :: thesis: x in A1 . k
A3: ( n in NAT & k in NAT ) by ORDINAL1:def 13;
Partial_Intersection A1 is non-ascending by Th12;
then A4: (Partial_Intersection A1) . n c= (Partial_Intersection A1) . k by A2, A3, PROB_1:def 6;
(Partial_Intersection A1) . k c= A1 . k by Th10;
then (Partial_Intersection A1) . n c= A1 . k by A4, XBOOLE_1:1;
hence x in A1 . k by A1; :: thesis: verum

end;

hence for k being Nat st k <= n holds
x in A1 . k ; :: thesis: verum

end;

defpred S₁[ Nat] means ( ( for k being Nat st k <= $1 holds
x in A1 . k ) implies x in (Partial_Intersection A1) . $1 );
A5: S₁[ 0 ]

proof

assume for k being Nat st k <= 0 holds
x in A1 . k ; :: thesis: x in (Partial_Intersection A1) . 0
then x in A1 . 0 ;
hence x in (Partial_Intersection A1) . 0 by Def1; :: thesis: verum

end;

A6: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: ( ( for k being Nat st k <= i holds
x in A1 . k ) implies x in (Partial_Intersection A1) . i ) ; :: thesis: S₁[i + 1]
assume A8: for k being Nat st k <= i + 1 holds
x in A1 . k ; :: thesis: x in (Partial_Intersection A1) . (i + 1)
then A9: for k being Nat st k <= i holds
x in A1 . k by NAT_1:12;
A10: x in A1 . (i + 1) by A8;
(Partial_Intersection A1) . (i + 1) = ((Partial_Intersection A1) . i) /\ (A1 . (i + 1)) by Def1;
hence x in (Partial_Intersection A1) . (i + 1) by A7, A9, A10, XBOOLE_0:def 4; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
hence ( ( for k being Nat st k <= n holds
x in A1 . k ) implies x in (Partial_Intersection A1) . n ) ; :: thesis: verum