let F, G be ext-real-membered set ; :: thesis: for r being Real st r ++ F = r ++ G holds
F = G
let r be Real; :: thesis: ( r ++ F = r ++ G implies F = G )
assume r ++ F = r ++ G ; :: thesis: F = G
then ( F c= G & G c= F ) by Th135;
hence F = G ; :: thesis: verum