let F, G be ext-real-membered set ; :: thesis: ( F c= G iff -- F c= -- G )
( -- (-- F) = F & -- (-- G) = G ) ;
hence ( F c= G iff -- F c= -- G ) by Lm1; :: thesis: verum