{ r where r is Element of T : deg r <= i } c= Union the Sorts of T

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { r where r is Element of T : deg r <= i } or a in Union the Sorts of T )
assume a in { r where r is Element of T : deg r <= i } ; :: thesis: a in Union the Sorts of T
then ex r being Element of T st
( a = r & deg r <= i ) ;
hence a in Union the Sorts of T ; :: thesis: verum

end;

hence { r where r is Element of T : deg r <= i } is Subset of T ; :: thesis: verum