let X be rational-membered set ; :: thesis: ( ( for w being rational number holds w in X ) implies X = RAT )
assume A1: for w being rational number holds w in X ; :: thesis: X = RAT
thus X c= RAT by Th4; :: according to XBOOLE_0:def 10 :: thesis: RAT c= X
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in RAT or e in X )
assume e in RAT ; :: thesis: e in X
then e is rational ;
hence e in X by A1; :: thesis: verum