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