let F, G be ext-real-membered set ; :: thesis: (F /\ G) "" c= (F "") /\ (G "")
let i be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not i in (F /\ G) "" or i in (F "") /\ (G "") )
assume i in (F /\ G) "" ; :: thesis: i in (F "") /\ (G "")
then consider w being Element of ExtREAL such that
A1: i = w " and
A2: w in F /\ G ;
w in G by A2, XBOOLE_0:def 4;
then A3: w " in G "" ;
w in F by A2, XBOOLE_0:def 4;
then w " in F "" ;
hence i in (F "") /\ (G "") by A1, A3, XBOOLE_0:def 4; :: thesis: verum