thus NatDivisors 1 c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= NatDivisors 1
proof
let x be object ; :: 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:15;
hence x in {1} by A1, ZFMISC_1:31; :: thesis: verum
end;
let x be object ; :: 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