let S1, S2 be non empty set ; :: thesis: ( ( for x being set holds
( x in S1 iff x is non empty IntervalSet of U ) ) & ( for x being set holds
( x in S2 iff x is non empty IntervalSet of U ) ) implies S1 = S2 )
assume that
A1: for x being set holds
( x in S1 iff x is non empty IntervalSet of U ) and
A2: for x being set holds
( x in S2 iff x is non empty IntervalSet of U ) ; :: thesis: S1 = S2
for x being set holds
( x in S1 iff x in S2 )

proof

let x be set ; :: thesis: ( x in S1 iff x in S2 )
thus ( x in S1 implies x in S2 ) :: thesis: ( x in S2 implies x in S1 )

proof

assume x in S1 ; :: thesis: x in S2
then x is non empty IntervalSet of U by A1;
hence x in S2 by A2; :: thesis: verum

end;

assume x in S2 ; :: thesis: x in S1
then x is non empty IntervalSet of U by A2;
hence x in S1 by A1; :: thesis: verum

end;

hence S1 = S2 by TARSKI:2; :: thesis: verum