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 j be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not j in -- F or j in -- G )
assume j in -- F ; :: thesis: j in -- G
then - j in F by Th2;
hence j in -- G by A1, Th2; :: thesis: verum