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