let D1, D2 be set ; :: thesis: ( D1 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
D1 c= D ) & D2 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
D2 c= D ) implies D1 = D2 )
assume A48: ( D1 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
D1 c= D ) & D2 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
D2 c= D ) ) ; :: thesis: D1 = D2
thus ( D1 c= D2 & D2 c= D1 ) by A48; :: according to XBOOLE_0:def 10 :: thesis: verum