let K1 be Subfield of F_Rat ; :: thesis: INT c= the carrier of K1
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in INT or m in the carrier of K1 )
assume m in INT ; :: thesis: m in the carrier of K1
then reconsider m = m as Integer ;
set C1 = the carrier of K1;
A1: NAT c= the carrier of K1 by Th23;

per cases ( 0 <= m or 0 > m ) ;

suppose 0 <= m ; :: thesis: m in the carrier of K1

hence m in the carrier of K1 by A1, INT_1:3; :: thesis: verum

end;

suppose 0 > m ; :: thesis: m in the carrier of K1

then reconsider mm = - m as Element of NAT by INT_1:3;
reconsider mmm = mm as Element of K1 by A1;
consider mm1 being Element of K1 such that
A2: mmm + mm1 = 0. K1 by ALGSTR_0:def 11;
A3: the carrier of K1 c= the carrier of F_Rat by EC_PF_1:def 1;
then reconsider mm2 = mm1 as Element of F_Rat ;
reconsider mm3 = mm as Element of F_Rat by A2, A3;
mm3 + mm2 = 0. K1 by A2, Th17
.= 0. F_Rat by EC_PF_1:def 1 ;
then mm2 = - mm ;
hence m in the carrier of K1 ; :: thesis: verum

end;

end;