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, 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 XXREAL_3:92;
then A4: i = - (w * (- w1)) by A1;
- w1 in G by A3, Th2;
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 Th2;
then consider w, w1 being Element of ExtREAL such that
A5: ( - i = w * w1 & w in F ) and
A6: w1 in G ;
( w * (- w1) = - (w * w1) & - w1 in -- G ) by A6, XXREAL_3:92;
hence i in F ** (-- G) by A5; :: thesis: verum