let F, G be ext-real-membered set ; :: thesis: ( F c= G implies F "" c= G "" )
assume A1: F c= 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 ex w being Element of ExtREAL st
( i = w " & w in F ) ;
hence i in G "" by A1; :: thesis: verum