let n be natural number ; :: thesis: NAT \ { t where t is Element of NAT : n <= t } is finite
NAT \ { t where t is Element of NAT : n <= t } c= n + 1

proof

NAT \ { t where t is Element of NAT : n <= t } c= (Seg n) \/ {0}

proof

set S = NAT \ { t where t is Element of NAT : n <= t } ;

per cases ( n = 0 or n > 0 ) ;

suppose A1: n = 0 ; :: thesis: NAT \ { t where t is Element of NAT : n <= t } c= (Seg n) \/ {0}

NAT \ { t where t is Element of NAT : n <= t } is empty

proof

let x be object ; :: according to XBOOLE_0:def 1 :: thesis: not x in NAT \ { t where t is Element of NAT : n <= t }
assume A2: x in NAT \ { t where t is Element of NAT : n <= t } ; :: thesis: contradiction
( x in NAT & not x in { t where t is Element of NAT : 0 <= t } ) by A1, A2, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum

end;

hence NAT \ { t where t is Element of NAT : n <= t } c= (Seg n) \/ {0} ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: NAT \ { t where t is Element of NAT : n <= t } c= (Seg n) \/ {0}

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT \ { t where t is Element of NAT : n <= t } or x in (Seg n) \/ {0} )
assume A3: x in NAT \ { t where t is Element of NAT : n <= t } ; :: thesis: x in (Seg n) \/ {0}
A4: ( x in NAT & not x in { t where t is Element of NAT : n <= t } ) by A3, XBOOLE_0:def 5;
reconsider x = x as Element of NAT by A3;
A5: ( x = 0 or x in Seg x ) by FINSEQ_1:3;
x <= n by A4;
then Seg x c= Seg n by FINSEQ_1:5;
then ( x in {0} or x in Seg n ) by A5, TARSKI:def 1;
hence x in (Seg n) \/ {0} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence NAT \ { t where t is Element of NAT : n <= t } c= n + 1 by AFINSQ_1:4; :: thesis: verum

end;

hence NAT \ { t where t is Element of NAT : n <= t } is finite ; :: thesis: verum