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;