let A, B, C be set ; :: thesis: for p being object st A c= B & B /\ C = {p} & p in A holds
A /\ C = {p}
let p be object ; :: 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} )
p in B /\ C by A2, TARSKI:def 1;
then A3: p in C by XBOOLE_0:def 4;
assume p in A ; :: thesis: A /\ C = {p}
then p in A /\ C by A3, XBOOLE_0:def 4;
hence A /\ C = {p} by A2, Lm3, A1, XBOOLE_1:26; :: thesis: verum