let n be Nat; :: thesis: for X being set
for A1 being SetSequence of X
for x being object holds
( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )
let X be set ; :: thesis: for A1 being SetSequence of X
for x being object 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: for x being object holds
( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )
let x be object ; :: thesis: ( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )
defpred S₁[ Nat] means ( ( for k being Nat st k <= $1 holds
x in A1 . k ) implies x in (Partial_Intersection A1) . $1 );
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

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

end;

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 A4: 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

A5: Partial_Intersection A1 is non-ascending by Th10;
let k be Nat; :: thesis: ( k <= n implies x in A1 . k )
assume A6: k <= n ; :: thesis: x in A1 . k
A7: (Partial_Intersection A1) . k c= A1 . k by Th8;
(Partial_Intersection A1) . n c= (Partial_Intersection A1) . k by A6, A5, PROB_1:def 4;
then (Partial_Intersection A1) . n c= A1 . k by A7;
hence x in A1 . k by A4; :: thesis: verum

end;

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

end;

A8: 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;

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