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_{1}[ 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_{1}[i] holds

S_{1}[i + 1]

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

x in A1 . k ) implies x in (Partial_Intersection A1) . n )_{1}[ 0 ]
_{1}[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

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

x in A1 . k ) implies x in (Partial_Intersection A1) . $1 );

A1: for i being Nat st S

S

proof

thus
( x in (Partial_Intersection A1) . n implies for k being Nat st k <= n holds
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[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_{1}[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;assume A2: ( ( for k being Nat st k <= i holds

x in A1 . k ) implies x in (Partial_Intersection A1) . i ) ; :: thesis: S

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

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

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

x in A1 . k ; :: thesis: verum

end;x in A1 . k

for k being Nat st k <= n holds

x in A1 . k

proof

hence
for k being Nat st k <= n holds
A5:
Partial_Intersection A1 is V74()
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;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

x in A1 . k ; :: thesis: verum

proof

for n being Nat holds S
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;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

hence ( ( for k being Nat st k <= n holds

x in A1 . k ) implies x in (Partial_Intersection A1) . n ) ; :: thesis: verum