A2: not 1 in {0} by TARSKI:def 1;
1 in Segm n by A1, NAT_1:44;
hence (Segm n) \ {0} is non empty finite Subset of NAT by A2, XBOOLE_0:def 5; :: thesis: verum