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
A5: for x being Element of R holds
( x in it1 iff ( x < v or v < x ) ) and
A6: 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 object ; :: thesis: ( x in it1 implies x in it2 )
assume A7: x in it1 ; :: thesis: x in it2
then reconsider xp1 = x as Element of R ;
( xp1 < v or v < xp1 ) by A5, A7;
hence x in it2 by A6; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in it2 or x in it1 )
assume A8: x in it2 ; :: thesis: x in it1
then reconsider xp1 = x as Element of R ;
( xp1 < v or v < xp1 ) by A6, A8;
hence x in it1 by A5; :: thesis: verum