thus ( X c= Y implies for r being real number st r in X holds
r in Y ) ; :: thesis: ( ( for r being real number st r in X holds
r in Y ) implies X c= Y )
assume A1: for r being real number st r in X holds
r in Y ; :: thesis: X c= Y
let e be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( e in X implies e in Y )
assume e in X ; :: thesis: e in Y
hence e in Y by A1; :: thesis: verum