let X be set ; :: thesis:
let A1, A2 be SetSequence of X; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in (Intersection A1) \/ (Intersection A2) ; :: thesis:

per cases by A1, XBOOLE_0:def 3;

suppose A2: x in Intersection A1 ; :: thesis:

let k be Nat; :: thesis:
x in A1 . k by A2, PROB_1:13;
then x in (A1 . k) \/ (A2 . k) by XBOOLE_0:def 3;
hence x in (A1 (\/) A2) . k by Def2; :: thesis:

end;

hence x in Intersection (A1 (\/) A2) by PROB_1:13; :: thesis:

end;

suppose A3: x in Intersection A2 ; :: thesis:

let k be Nat; :: thesis:
x in A2 . k by A3, PROB_1:13;
then x in (A1 . k) \/ (A2 . k) by XBOOLE_0:def 3;
hence x in (A1 (\/) A2) . k by Def2; :: thesis:

end;

hence x in Intersection (A1 (\/) A2) by PROB_1:13; :: thesis:

end;

end;