let n be Nat; :: thesis: for x being object st n = {x} holds
x = 0
let x be object ; :: thesis: ( n = {x} implies x = 0 )
assume A1: n = {x} ; :: thesis: x = 0
then card n = 1 by CARD_1:30;
then x in {0} by A1, CARD_1:49, TARSKI:def 1;
hence x = 0 by TARSKI:def 1; :: thesis: verum