let x, A, B be set ; :: thesis: ( x in A /\ B implies In x,A = In x,B )
assume A1: x in A /\ B ; :: thesis: In x,A = In x,B
then A2: x in B by XBOOLE_0:def 4;
x in A by A1, XBOOLE_0:def 4;
hence In x,A = x by Def1
.= In x,B by A2, Def1 ;
:: thesis: verum