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