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

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;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