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 - i in F \/ G by Th2;
then ( - i in F or - i in G ) by XBOOLE_0:def 3;
then ( i in -- F or i in -- G ) by Th2;
hence i in (-- F) \/ (-- G) by XBOOLE_0:def 3; :: thesis: verum

end;

assume i in (-- F) \/ (-- G) ; :: thesis: i in -- (F \/ G)
then ( i in -- F or i in -- G ) by XBOOLE_0:def 3;
then ( - i in F or - i in G ) by Th2;
then - i in F \/ G by XBOOLE_0:def 3;
hence i in -- (F \/ G) by Th2; :: thesis: verum