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 S1[ object ] 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 S1[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 S1[x] ) ; :: thesis: X = Y
for x being object holds
( x in X iff x in Y )
proof
let x be object ; :: 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 S1[x] by A6;
hence x in Y by A7; :: thesis: verum
end;
assume x in Y ; :: thesis: x in X
then S1[x] by A7;
hence x in X by A6; :: thesis: verum
end;
hence X = Y by TARSKI:2; :: thesis: verum