{ t where t is Element of NAT : ( 0 <= t & t <= T ) } c= REAL

proof

hence
{ t where t is Element of NAT : ( 0 <= t & t <= T ) } is Subset of REAL
; :: thesis: verum
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { t where t is Element of NAT : ( 0 <= t & t <= T ) } or q in REAL )

assume q in { t where t is Element of NAT : ( 0 <= t & t <= T ) } ; :: thesis: q in REAL

then consider q1 being Element of NAT such that

C1: ( q = q1 & 0 <= q1 & q1 <= T ) ;

thus q in REAL by NUMBERS:19, C1; :: thesis: verum

end;assume q in { t where t is Element of NAT : ( 0 <= t & t <= T ) } ; :: thesis: q in REAL

then consider q1 being Element of NAT such that

C1: ( q = q1 & 0 <= q1 & q1 <= T ) ;

thus q in REAL by NUMBERS:19, C1; :: thesis: verum