assume [x,y] is natural ; :: thesis: contradiction
then reconsider n = [x,y] as Nat ;
card n <= 2 by Th49;
then n <= 2 ;
then not not n = 0 & ... & not n = 2 ;

per cases then ( n = 0 or n = 1 or n = 2 ) ;

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;