let X be set ; :: thesis: for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1

let A1 be SetSequence of X; :: thesis: Intersection (Partial_Intersection A1) = Intersection A1

thus Intersection (Partial_Intersection A1) c= Intersection A1 :: according to XBOOLE_0:def 10 :: thesis: Intersection A1 c= Intersection (Partial_Intersection A1)

assume A2: x in Intersection A1 ; :: thesis: x in Intersection (Partial_Intersection A1)

for n being Nat holds x in (Partial_Intersection A1) . n

let A1 be SetSequence of X; :: thesis: Intersection (Partial_Intersection A1) = Intersection A1

thus Intersection (Partial_Intersection A1) c= Intersection A1 :: according to XBOOLE_0:def 10 :: thesis: Intersection A1 c= Intersection (Partial_Intersection A1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection A1 or x in Intersection (Partial_Intersection A1) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection (Partial_Intersection A1) or x in Intersection A1 )

assume A1: x in Intersection (Partial_Intersection A1) ; :: thesis: x in Intersection A1

for n being Nat holds x in A1 . n

end;assume A1: x in Intersection (Partial_Intersection A1) ; :: thesis: x in Intersection A1

for n being Nat holds x in A1 . n

proof

hence
x in Intersection A1
by PROB_1:13; :: thesis: verum
let n be Nat; :: thesis: x in A1 . n

x in (Partial_Intersection A1) . n by A1, PROB_1:13;

hence x in A1 . n by Th12; :: thesis: verum

end;x in (Partial_Intersection A1) . n by A1, PROB_1:13;

hence x in A1 . n by Th12; :: thesis: verum

assume A2: x in Intersection A1 ; :: thesis: x in Intersection (Partial_Intersection A1)

for n being Nat holds x in (Partial_Intersection A1) . n

proof

hence
x in Intersection (Partial_Intersection A1)
by PROB_1:13; :: thesis: verum
let n be Nat; :: thesis: x in (Partial_Intersection A1) . n

for k being Nat st k <= n holds

x in A1 . k by A2, PROB_1:13;

hence x in (Partial_Intersection A1) . n by Th12; :: thesis: verum

end;for k being Nat st k <= n holds

x in A1 . k by A2, PROB_1:13;

hence x in (Partial_Intersection A1) . n by Th12; :: thesis: verum