let n, m be Nat; :: thesis: ( n divides m implies NatDivisors n c= NatDivisors m )
assume A1: n divides m ; :: thesis: NatDivisors n c= NatDivisors m
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NatDivisors n or x in NatDivisors m )
assume A2: x in NatDivisors n ; :: thesis: x in NatDivisors m
reconsider x = x as Nat by A2;
( 0 < x & x divides n ) by A2, MOEBIUS1:39;
hence x in NatDivisors m by A1, INT_2:9, MOEBIUS1:39; :: thesis: verum