let p be Prime; :: thesis: Moebius p = - 1
reconsider p1 = p as prime Element of NAT by ORDINAL1:def 12;
Moebius p = (- 1) |^ (card (support (ppf p1))) by Def3
.= (- 1) |^ (card {p}) by Th8
.= (- 1) |^ 1 by CARD_1:30 ;
hence Moebius p = - 1 ; :: thesis: verum