let X, Y be Subset of (Class (CompClass E,(CComp s1))); :: thesis: ( ( for z being set holds
( z in X iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) ) ) & ( for z being set holds
( z in Y iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) ) ) implies X = Y )
defpred S₁[ set ] means ex x being set st
( x in the Sorts of A . s1 & $1 = Class (CompClass E,(CComp s1)),x );
assume A6: for x being set holds
( x in X iff S₁[x] ) ; :: thesis: ( ex z being set st
( ( z in Y implies ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) ) implies ( ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) & not z in Y ) ) or X = Y )
assume A7: for x being set holds
( x in Y iff S₁[x] ) ; :: thesis: X = Y
for x being set holds
( x in X iff x in Y )

proof

let x be set ; :: thesis: ( x in X iff x in Y )

hereby :: thesis: ( x in Y implies x in X )

assume x in X ; :: thesis: x in Y
then S₁[x] by A6;
hence x in Y by A7; :: thesis: verum

end;

assume x in Y ; :: thesis: x in X
then S₁[x] by A7;
hence x in X by A6; :: thesis: verum

end;

hence X = Y by TARSKI:2; :: thesis: verum