let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\+\) A1) c= A \+\ (Intersection A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds Intersection (A (\+\) A1) c= A \+\ (Intersection A1)
let A1 be SetSequence of X; :: thesis: Intersection (A (\+\) A1) c= A \+\ (Intersection A1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersection (A (\+\) A1) or x in A \+\ (Intersection A1) )
assume A1: x in Intersection (A (\+\) A1) ; :: thesis: x in A \+\ (Intersection A1)
A2: now :: thesis: for n being Nat holds
( ( x in A & not x in A1 . n ) or ( not x in A & x in A1 . n ) )
let n be Nat; :: thesis: ( ( x in A & not x in A1 . n ) or ( not x in A & x in A1 . n ) )
x in (A (\+\) A1) . n by A1, PROB_1:13;
then x in A \+\ (A1 . n) by Def9;
hence ( ( x in A & not x in A1 . n ) or ( not x in A & x in A1 . n ) ) by XBOOLE_0:1; :: thesis: verum
end;
assume not x in A \+\ (Intersection A1) ; :: thesis: contradiction
then A3: ( ( not x in A & not x in Intersection A1 ) or ( x in Intersection A1 & x in A ) ) by XBOOLE_0:1;
per cases ( ( not x in A & not for n being Nat holds x in A1 . n ) or ( x in A & ( for n being Nat holds x in A1 . n ) ) ) by A3, PROB_1:13;
suppose ( not x in A & not for n being Nat holds x in A1 . n ) ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum
end;
suppose A4: ( x in A & ( for n being Nat holds x in A1 . n ) ) ; :: thesis: contradiction
then x in A1 . 0 ;
hence contradiction by A2, A4; :: thesis: verum
end;
end;