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 Th155;
hence F = G ; :: thesis: verum