thus NatDivisors 1 c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= NatDivisors 1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NatDivisors 1 or x in {1} )
assume x in NatDivisors 1 ; :: thesis: x in {1}
then consider k being Element of NAT such that
A1: x = k and
k <> 0 and
A2: k divides 1 ;
k = 1 by A2, WSIERP_1:20;
hence x in {1} by A1, ZFMISC_1:37; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in NatDivisors 1 )
assume A3: x in {1} ; :: thesis: x in NatDivisors 1
then reconsider m = x as Element of NAT ;
( m <> 0 & m divides 1 ) by A3, TARSKI:def 1;
hence x in NatDivisors 1 ; :: thesis: verum