Moebius 3 = (- 1) |^ (card (support (ppf 3))) by Def3, PEPIN:41
.= (- 1) |^ (card {3}) by Th8, PEPIN:41
.= (- 1) |^ 1 by CARD_1:30 ;
hence Moebius 3 = - 1 ; :: thesis: verum