let A, B be complex-membered set ; :: thesis: ( A c= B iff -- A c= -- B )
( -- (-- A) = A & -- (-- B) = B ) ;
hence ( A c= B iff -- A c= -- B ) by Lm2; :: thesis: verum