let X be set ; :: thesis: for F, G being ext-real-membered set st X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds
X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
let F, G be ext-real-membered set ; :: thesis: ( X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } implies X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } )
assume A1: X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; :: thesis: X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
thus X c= { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } :: according to XBOOLE_0:def 10 :: thesis: { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } c= X

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in X or e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } )
assume e in X ; :: thesis: e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
then ex w1, w2 being Element of ExtREAL st
( e = w1 * w2 & w1 in F & w2 in G ) by A1;
hence e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } or e in X )
assume e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; :: thesis: e in X
then ex w1, w2 being Element of ExtREAL st
( e = w1 * w2 & w1 in G & w2 in F ) ;
hence e in X by A1; :: thesis: verum