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