let p be Prime; :: thesis: #divs p = 2
set X = NatDivisors p;
D2: EXP 0 = NAT --> 1 by ThEXP0;
D1: NatDivisors p = {1,p} by LATSTONE:26;
D3: #divs p = Sum ((EXP 0) | (NatDivisors p)) by NAT_5:def 2;
1 <> p by INT_2:def 4;
then card (NatDivisors p) = 2 by D1, CARD_2:57;
hence #divs p = 2 by D3, D2, LemmaCard; :: thesis: verum