let n be Nat; :: thesis: for R being NatRelStr of n
for m being Nat st n <= m & m < 2 * n holds
( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )
let R be NatRelStr of n; :: thesis: for m being Nat st n <= m & m < 2 * n holds
( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )
let m be Nat; :: thesis: ( n <= m & m < 2 * n implies ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) ) )
assume that
A1: n <= m and
A2: m < 2 * n ; :: thesis: ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
A3: the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by Def9;
A4: m in (Segm (2 * n)) \ (Segm n) by A1, A2, Th2;
A5: 2 * n in {(2 * n)} by TARSKI:def 1;
then [m,(2 * n)] in [:((2 * n) \ n),{(2 * n)}:] by A4, ZFMISC_1:def 2;
hence [m,(2 * n)] in the InternalRel of (Mycielskian R) by A3, XBOOLE_0:def 3; :: thesis: [(2 * n),m] in the InternalRel of (Mycielskian R)
[(2 * n),m] in [:{(2 * n)},((2 * n) \ n):] by A4, A5, ZFMISC_1:def 2;
hence [(2 * n),m] in the InternalRel of (Mycielskian R) by A3, Th4; :: thesis: verum