let A, B be complex-membered set ; :: thesis: ( A "" = B "" implies A = B )
assume A "" = B "" ; :: thesis: A = B
then ( A c= B & B c= A ) by Th30;
hence A = B ; :: thesis: verum