let X be set ; :: thesis: ( X is integer-membered implies X is rational-membered )
assume A2: X is integer-membered ; :: thesis: X is rational-membered
let x be object ; :: according to MEMBERED:def 4 :: thesis: ( x in X implies x is rational )
assume x in X ; :: thesis: x is rational
then x is integer by A2;
then x in INT ;
hence x in RAT by NUMBERS:14; :: according to RAT_1:def 2 :: thesis: verum