let F, G be ext-real-membered set ; :: thesis: (F /\ G) "" c= (F "" ) /\ (G "" )
let i be ext-real number ; :: 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 F & w in G ) by A2, XBOOLE_0:def 4;
then ( w " in F "" & w " in G "" ) ;
hence i in (F "" ) /\ (G "" ) by A1, XBOOLE_0:def 4; :: thesis: verum