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)
proof
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
proof
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;
hence x in Intersection A1 by PROB_1:13; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection A1 or x in 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
proof
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;
hence x in Intersection (Partial_Intersection A1) by PROB_1:13; :: thesis: verum