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

let A1 be SetSequence of X; :: thesis: Partial_Intersection A1 is V74()

let A1 be SetSequence of X; :: thesis: Partial_Intersection A1 is V74()

now :: thesis: for n being Nat holds (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n

hence
Partial_Intersection A1 is V74()
by PROB_2:6; :: thesis: verumlet n be Nat; :: thesis: (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n

(Partial_Intersection A1) . (n + 1) = ((Partial_Intersection A1) . n) /\ (A1 . (n + 1)) by Def1;

hence (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n by XBOOLE_1:17; :: thesis: verum

end;(Partial_Intersection A1) . (n + 1) = ((Partial_Intersection A1) . n) /\ (A1 . (n + 1)) by Def1;

hence (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n by XBOOLE_1:17; :: thesis: verum