let F, G be ext-real-membered set ; :: thesis: for r being Real st r -- F c= r -- G holds
F c= G
let r be Real; :: thesis: ( r -- F c= r -- G implies F c= G )
assume A1: r -- F c= r -- G ; :: thesis: F c= G
let i be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not i in F or i in G )
assume i in F ; :: thesis: i in G
then r - i in r -- F by Th152;
then ex w being Element of ExtREAL st
( r - i = r - w & w in G ) by A1, Th154;
hence i in G by XXREAL_3:12; :: thesis: verum