let F, G be ext-real-membered set ; :: thesis: for r being real number st r -- F = r -- G holds
F = G
let r be real number ; :: 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 by XBOOLE_0:def 10; :: thesis: verum