let A, B, C be set ; :: thesis: ( A = B \/ C & A c= B implies A = B )
assume A1: ( A = B \/ C & A c= B ) ; :: thesis: A = B
then B c= A by XBOOLE_1:7;
hence A = B by A1, XBOOLE_0:def 10; :: thesis: verum