let X, Y be set ; :: thesis: for x being object st x in X /\ Y holds
In (x,X) = In (x,Y)
let x be object ; :: thesis: ( x in X /\ Y implies In (x,X) = In (x,Y) )
assume A1: x in X /\ Y ; :: thesis: In (x,X) = In (x,Y)
then A2: x in Y by XBOOLE_0:def 4;
x in X by A1, XBOOLE_0:def 4;
hence In (x,X) = x by Def7
.= In (x,Y) by A2, Def7 ;
:: thesis: verum