let x be set ; :: according to FRAENKEL:def 1 :: 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