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

A2: for x being set holds

( x in S1 iff x is non empty IntervalSet of U ) and

A3: for x being set holds

( x in S2 iff x is non empty IntervalSet of U ) ; :: thesis: S1 = S2

for x being object holds

( x in S1 iff x in S2 ) by A3, A2;

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

( 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

A2: for x being set holds

( x in S1 iff x is non empty IntervalSet of U ) and

A3: for x being set holds

( x in S2 iff x is non empty IntervalSet of U ) ; :: thesis: S1 = S2

for x being object holds

( x in S1 iff x in S2 ) by A3, A2;

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