let F, G be ext-real-membered set ; :: thesis: ( -- F = -- G implies F = G )
assume -- F = -- G ; :: thesis: F = G
then ( F c= G & G c= F ) by Th3;
hence F = G ; :: thesis: verum