let F, G be ext-real-membered set ; :: thesis: (F \/ G) "" = (F "") \/ (G "")
let i be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not i in (F \/ G) "" or i in (F "") \/ (G "") ) & ( not i in (F "") \/ (G "") or i in (F \/ G) "" ) )

hereby :: 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 or w in G ) by A2, XBOOLE_0:def 3;
then ( w " in F "" or w " in G "" ) ;
hence i in (F "") \/ (G "") by A1, XBOOLE_0:def 3; :: thesis: verum

end;

assume A3: i in (F "") \/ (G "") ; :: thesis: i in (F \/ G) ""

per cases ( i in F "" or i in G "" ) by A3, XBOOLE_0:def 3;

suppose i in F "" ; :: thesis: i in (F \/ G) ""

then consider w being Element of ExtREAL such that
A4: i = w " and
A5: w in F ;
w in F \/ G by A5, XBOOLE_0:def 3;
hence i in (F \/ G) "" by A4; :: thesis: verum

end;

suppose i in G "" ; :: thesis: i in (F \/ G) ""

then consider w being Element of ExtREAL such that
A6: i = w " and
A7: w in G ;
w in F \/ G by A7, XBOOLE_0:def 3;
hence i in (F \/ G) "" by A6; :: thesis: verum

end;

end;