let F, G, H, I be ext-real-membered set ; :: thesis: ( F c= G & H c= I implies F -- H c= G -- I )
assume A1: ( F c= G & H c= I ) ; :: thesis: F -- H c= G -- I
let i be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not i in F -- H or i in G -- I )
A2: F -- H = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in H ) } by Th54;
assume i in F -- H ; :: thesis: i in G -- I
then ex w, w1 being Element of ExtREAL st
( i = w - w1 & w in F & w1 in H ) by A2;
hence i in G -- I by A1, Th55; :: thesis: verum