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