let F, G be ext-real-membered set ; :: thesis: -- (F ++ G) = (-- F) ++ (-- G)
let j be ext-real number ; :: 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 Lm1;
( - 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 ) ;
A8: - (w1 + w2) = (- w1) - w2 by Lm1;
( - w1 in F & - w2 in G ) by A7, Th8;
then (- w1) + (- w2) in F ++ G ;
hence j in -- (F ++ G) by A6, A8, Th8; :: thesis: verum