let A, B, C, p be set ; :: thesis: ( A c= B & B /\ C = {p} & p in A implies A /\ C = {p} )
assume A1: A c= B ; :: thesis: ( not B /\ C = {p} or not p in A or A /\ C = {p} )
assume A2: B /\ C = {p} ; :: thesis: ( not p in A or A /\ C = {p} )
then p in B /\ C by TARSKI:def 1;
then A3: p in C by XBOOLE_0:def 4;
assume p in A ; :: thesis: A /\ C = {p}
then A4: p in A /\ C by A3, XBOOLE_0:def 4;
A /\ C c= {p} by A1, A2, XBOOLE_1:26;
hence A /\ C = {p} by A4, Lm3; :: thesis: verum