let IT1, IT2 be Subset of ; :: thesis: ( ( for e being set holds
( e in IT1 iff e DSJoins X,Y,G ) ) & ( for e being set holds
( e in IT2 iff e DSJoins X,Y,G ) ) implies IT1 = IT2 )
assume that
A7: for e being set holds
( e in IT1 iff e DSJoins X,Y,G ) and
A8: for e being set holds
( e in IT2 iff e DSJoins X,Y,G ) ; :: thesis: IT1 = IT2

now

let e be set ; :: thesis: ( e in IT2 iff e in IT1 )
( e in IT1 iff e DSJoins X,Y,G ) by A7;
hence ( e in IT2 iff e in IT1 ) by A8; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:2; :: thesis: verum