set D = { x where x is Element of R : ( x < v or v < x ) } ;
set cR = the carrier of R;
set iR = the InternalRel of R;
{ x where x is Element of R : ( x < v or v < x ) } c= the carrier of R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of R : ( x < v or v < x ) } or x in the carrier of R )
assume x in { x where x is Element of R : ( x < v or v < x ) } ; :: thesis: x in the carrier of R
then consider a being Element of R such that
A1: x = a and
A2: ( a < v or v < a ) ;
per cases ( a < v or v < a ) by A2;
suppose a < v ; :: thesis: x in the carrier of R
then a <= v by ORDERS_2:def 6;
then [a,v] in the InternalRel of R by ORDERS_2:def 5;
then [a,v] in [: the carrier of R, the carrier of R:] ;
hence x in the carrier of R by A1, ZFMISC_1:87; :: thesis: verum
end;
suppose v < a ; :: thesis: x in the carrier of R
then v <= a by ORDERS_2:def 6;
then [v,a] in the InternalRel of R by ORDERS_2:def 5;
then [v,a] in [: the carrier of R, the carrier of R:] ;
hence x in the carrier of R by A1, ZFMISC_1:87; :: thesis: verum
end;
end;
end;
then reconsider D = { x where x is Element of R : ( x < v or v < x ) } as Subset of R ;
take D ; :: thesis: for x being Element of R holds
( x in D iff ( x < v or v < x ) )
let x be Element of R; :: thesis: ( x in D iff ( x < v or v < x ) )
hereby :: thesis: ( ( x < v or v < x ) implies x in D )
assume x in D ; :: thesis: ( x < v or v < x )
then consider a being Element of R such that
A3: x = a and
A4: ( a < v or v < a ) ;
thus ( x < v or v < x ) by A3, A4; :: thesis: verum
end;
assume ( x < v or v < x ) ; :: thesis: x in D
hence x in D ; :: thesis: verum