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