let X, Y be non empty set ; :: thesis: ( ( for x being set holds
( x in X iff ex N being strict LTLnode of v st x = N ) ) & ( for x being set holds
( x in Y iff ex N being strict LTLnode of v st x = N ) ) implies X = Y )
( ( for x being set holds
( x in X iff ex N being strict LTLnode of v st x = N ) ) & ( for x being set holds
( x in Y iff ex N being strict LTLnode of v st x = N ) ) implies X = Y )

proof

assume A1: ( ( for x being set holds
( x in X iff ex N being strict LTLnode of v st x = N ) ) & ( for x being set holds
( x in Y iff ex N being strict LTLnode of v st x = N ) ) ) ; :: 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 )
( x in X iff ex N being strict LTLnode of v st x = N ) by A1;
hence ( x in X iff x in Y ) by A1; :: thesis: verum

end;

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

end;

hence ( ( for x being set holds
( x in X iff ex N being strict LTLnode of v st x = N ) ) & ( for x being set holds
( x in Y iff ex N being strict LTLnode of v st x = N ) ) implies X = Y ) ; :: thesis: verum