assume [x,y] is natural ; :: thesis: contradiction
then reconsider n = [x,y] as natural number ;
card n <= 2 by Th69;
then A1: n <= 2 by CARD_1:def 2;

per cases ( n = 0 or n = 1 or n = 2 ) by A1, NAT_1:26;

suppose n = 0 ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose n = 1 ; :: thesis: contradiction

hence contradiction by CARD_1:49, ZFMISC_1:4; :: thesis: verum

end;

suppose n = 2 ; :: thesis: contradiction

hence contradiction by CARD_1:50, ZFMISC_1:6; :: thesis: verum

end;

end;