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 Th132;
then ex w being Element of ExtREAL st
( r + i = r + w & w in G ) by A1, Th134;
hence i in G by XXREAL_3:11; :: thesis: verum