thus dom (Cong m) c= INT ; :: according to PARTFUN1:def 2,XBOOLE_0:def 10 :: thesis: INT c= dom (Cong m)
thus INT c= dom (Cong m) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INT or x in dom (Cong m) )
assume x in INT ; :: thesis: x in dom (Cong m)
then reconsider x = x as Integer ;
x,x are_congruent_mod m by INT_1:11;
then [x,x] in Cong m by Def1;
hence x in dom (Cong m) by XTUPLE_0:def 12; :: thesis: verum
end;