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 A1: 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)}
consider k being Element of NAT such that
A2: k = a and
A3: k <= n + 1 by A1;
A4: ( k <= n or k = n + 1 ) by A3, NAT_1:8;
A5: ( a in { i where i is Element of NAT : i <= n } or a in {(n + 1)} ) by A2, A4, TARSKI:def 1;
thus a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} by A5, 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 A6: 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 }
A7: ( a in { i where i is Element of NAT : i <= n } or a in {(n + 1)} ) by A6, XBOOLE_0:def 3;
A8: ( ex i being Element of NAT st
( a = i & i <= n ) or a = n + 1 ) by A7, TARSKI:def 1;

A9: now

given i being Element of NAT such that A10: a = i and
A11: i <= n ; :: thesis: a in { k where k is Element of NAT : k <= n + 1 }
A12: n <= n + 1 by NAT_1:11;
A13: i <= n + 1 by A11, A12, XXREAL_0:2;
thus a in { k where k is Element of NAT : k <= n + 1 } by A10, A13; :: thesis: verum

end;

thus a in { k where k is Element of NAT : k <= n + 1 } by A8, A9; :: thesis: verum

end;