let X be set ; :: thesis: Tarski-Class {} c= Tarski-Class X
set T1 = Tarski-Class {};
set T2 = Tarski-Class X;
A1: ( Tarski-Class {} is_Tarski-Class_of {} & ( for D being set st D is_Tarski-Class_of {} holds
Tarski-Class {} c= D ) ) by CLASSES1:def 4;
( {} c= Tarski-Class X & Tarski-Class X is Tarski & not Tarski-Class X, {} are_equipotent ) by CARD_1:26;
then {} in Tarski-Class X ;
hence Tarski-Class {} c= Tarski-Class X by A1, CLASSES1:def 3; :: thesis: verum