theorem Th54: :: MEMBER_1:54

for F, G being ext-real-membered set holds F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }