let it1, it2 be Subset of R; :: thesis: ( ( for x being Element of R holds
( x in it1 iff ( x < v or v < x ) ) ) & ( for x being Element of R holds
( x in it2 iff ( x < v or v < x ) ) ) implies it1 = it2 )
assume that
A: for x being Element of R holds
( x in it1 iff ( x < v or v < x ) ) and
B: for x being Element of R holds
( x in it2 iff ( x < v or v < x ) ) ; :: thesis: it1 = it2

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: it2 c= it1

let x be set ; :: thesis: ( x in it1 implies x in it2 )
assume A1: x in it1 ; :: thesis: x in it2
then reconsider xp1 = x as Element of R ;
( xp1 < v or v < xp1 ) by A, A1;
hence x in it2 by B; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in it2 or x in it1 )
assume A1: x in it2 ; :: thesis: x in it1
then reconsider xp1 = x as Element of R ;
( xp1 < v or v < xp1 ) by B, A1;
hence x in it1 by A; :: thesis: verum