let X be set ; :: thesis: for A1, A2 being SetSequence of X holds (Intersection A1) \/ (Intersection A2) c= Intersection (A1 (\/) A2)
let A1, A2 be SetSequence of X; :: thesis: (Intersection A1) \/ (Intersection A2) c= Intersection (A1 (\/) A2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Intersection A1) \/ (Intersection A2) or x in Intersection (A1 (\/) A2) )
assume A1: x in (Intersection A1) \/ (Intersection A2) ; :: thesis: x in Intersection (A1 (\/) A2)

per cases ( x in Intersection A1 or x in Intersection A2 ) by A1, XBOOLE_0:def 3;

suppose A2: x in Intersection A1 ; :: thesis: x in Intersection (A1 (\/) A2)

now :: thesis: for k being Nat holds x in (A1 (\/) A2) . k

let k be Nat; :: thesis: x in (A1 (\/) A2) . k
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: verum

end;

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

end;

suppose A3: x in Intersection A2 ; :: thesis: x in Intersection (A1 (\/) A2)

now :: thesis: for k being Nat holds x in (A1 (\/) A2) . k

let k be Nat; :: thesis: x in (A1 (\/) A2) . k
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: verum

end;

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

end;

end;