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 Th13;
hence A = B ; :: thesis: verum