let X be set ; :: thesis: for U1 being Universe st U1 in Tarski-Class X holds
Tarski-Class U1 c= Tarski-Class X
let U1 be Universe; :: thesis: ( U1 in Tarski-Class X implies Tarski-Class U1 c= Tarski-Class X )
assume U1 in Tarski-Class X ; :: thesis: Tarski-Class U1 c= Tarski-Class X
then Tarski-Class X is_Tarski-Class_of U1 ;
hence Tarski-Class U1 c= Tarski-Class X by CLASSES1:def 4; :: thesis: verum