let F, G be ext-real-membered set ; :: thesis: F ** (-- G) = -- (F ** G)
let i be ext-real number ; :: 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, w1 being Element of ExtREAL such that
A1: i = w * w1 and
A2: w in F and
A3: w1 in -- G ;
w * (- w1) = - (w * w1) by EXTREAL1:26;
then A4: i = - (w * (- w1)) by A1;
- w1 in G by A3, Th8;
then w * (- w1) in F ** G by A2;
hence i in -- (F ** G) by A4; :: thesis: verum

end;

assume i in -- (F ** G) ; :: thesis: i in F ** (-- G)
then - i in F ** G by Th8;
then consider w, w1 being Element of ExtREAL such that
A5: - i = w * w1 and
A6: w in F and
A7: w1 in G ;
A8: w * (- w1) = - (w * w1) by EXTREAL1:26;
- w1 in -- G by A7;
hence i in F ** (-- G) by A5, A6, A8; :: thesis: verum