let A, B be Subset of X; :: thesis: ( x in A & A in S1 & x in B & B in S1 implies A = B )
assume A2: ( x in A & A in S1 & x in B & B in S1 ) ; :: thesis: A = B
then A meets B by XBOOLE_0:3;
hence A = B by A2, Def6; :: thesis: verum