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