let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in the carrier of T or x is set )
assume x in the carrier of T ; :: thesis: x is set
hence x is set ; :: thesis: verum