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 A2: r in X ; :: thesis: r in Y
thus r in Y by A1, A2; :: thesis: verum