let R be set ; :: thesis: ( R = RAT iff for x being object holds
( x in R iff ex m, n being Integer st x = m / n ) )
thus ( R = RAT implies for x being object holds
( x in R iff ex m, n being Integer st x = m / n ) ) by Lm4, Lm6; :: thesis: ( ( for x being object holds
( x in R iff ex m, n being Integer st x = m / n ) ) implies R = RAT )
assume A1: for x being object holds
( x in R iff ex m, n being Integer st x = m / n ) ; :: thesis: R = RAT
thus R c= RAT :: according to XBOOLE_0:def 10 :: thesis: RAT c= R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in RAT )
assume x in R ; :: thesis: x in RAT
then ex m, n being Integer st x = m / n by A1;
hence x in RAT by Lm6; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in RAT or x in R )
assume x in RAT ; :: thesis: x in R
then ex m, n being Integer st x = m / n by Lm4;
hence x in R by A1; :: thesis: verum