let n be Element of NAT ; :: thesis: { k where k is Element of NAT : k <= n + 1 } = { i where i is Element of NAT : i <= n } \/ {(n + 1)}
thus { k where k is Element of NAT : k <= n + 1 } c= { i where i is Element of NAT : i <= n } \/ {(n + 1)} :: according to XBOOLE_0:def 10 :: thesis: { i where i is Element of NAT : i <= n } \/ {(n + 1)} c= { k where k is Element of NAT : k <= n + 1 }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : k <= n + 1 } or a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} )
assume a in { k where k is Element of NAT : k <= n + 1 } ; :: thesis: a in { i where i is Element of NAT : i <= n } \/ {(n + 1)}
then consider k being Element of NAT such that
A1: k = a and
A2: k <= n + 1 ;
( k <= n or k = n + 1 ) by A2, NAT_1:8;
then ( a in { i where i is Element of NAT : i <= n } or a in {(n + 1)} ) by A1, TARSKI:def 1;
hence a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} by XBOOLE_0:def 3; :: thesis: verum

end;

thus { i where i is Element of NAT : i <= n } \/ {(n + 1)} c= { k where k is Element of NAT : k <= n + 1 } :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} or a in { k where k is Element of NAT : k <= n + 1 } )
assume a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} ; :: thesis: a in { k where k is Element of NAT : k <= n + 1 }
then ( a in { i where i is Element of NAT : i <= n } or a in {(n + 1)} ) by XBOOLE_0:def 3;
then A3: ( ex i being Element of NAT st
( a = i & i <= n ) or a = n + 1 ) by TARSKI:def 1;

now

given i being Element of NAT such that A4: a = i and
A5: i <= n ; :: thesis: a in { k where k is Element of NAT : k <= n + 1 }
n <= n + 1 by NAT_1:11;
then i <= n + 1 by A5, XXREAL_0:2;
hence a in { k where k is Element of NAT : k <= n + 1 } by A4; :: thesis: verum

end;

hence a in { k where k is Element of NAT : k <= n + 1 } by A3; :: thesis: verum

end;