let F, G be ext-real-membered set ; :: thesis: -- (F ++ G) = (-- F) ++ (-- G)
let j be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not j in -- (F ++ G) or j in (-- F) ++ (-- G) ) & ( not j in (-- F) ++ (-- G) or j in -- (F ++ G) ) )
hereby :: thesis: ( not j in (-- F) ++ (-- G) or j in -- (F ++ G) )
assume j in -- (F ++ G) ; :: thesis: j in (-- F) ++ (-- G)
then consider w being Element of ExtREAL such that
A1: j = - w and
A2: w in F ++ G ;
consider w1, w2 being Element of ExtREAL such that
A3: w = w1 + w2 and
A4: ( w1 in F & w2 in G ) by A2;
A5: - (w1 + w2) = (- w1) - w2 by XXREAL_3:9;
( - w1 in -- F & - w2 in -- G ) by A4;
hence j in (-- F) ++ (-- G) by A1, A3, A5; :: thesis: verum
end;
assume j in (-- F) ++ (-- G) ; :: thesis: j in -- (F ++ G)
then consider w1, w2 being Element of ExtREAL such that
A6: j = w1 + w2 and
A7: ( w1 in -- F & w2 in -- G ) ;
( - w1 in F & - w2 in G ) by A7, Th2;
then ( - (w1 + w2) = (- w1) - w2 & (- w1) + (- w2) in F ++ G ) by XXREAL_3:9;
hence j in -- (F ++ G) by A6, Th2; :: thesis: verum