let X be set ; :: thesis: ( X is rational-membered implies X c= RAT )
assume A1: X is rational-membered ; :: thesis: X c= RAT
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in RAT )
assume x in X ; :: thesis: x in RAT
then x is rational by A1;
hence x in RAT ; :: thesis: verum