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
A: n <= m and
B: 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);
D: 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 LMR;
E: m in (2 * n) \ n by A, B, Nat0;
F: 2 * n in {(2 * n)} by TARSKI:def 1;
then [m,(2 * n)] in [:((2 * n) \ n),{(2 * n)}:] by E, ZFMISC_1:def 2;
hence [m,(2 * n)] in the InternalRel of (Mycielskian R) by D, XBOOLE_0:def 3; :: thesis: [(2 * n),m] in the InternalRel of (Mycielskian R)
[(2 * n),m] in [:{(2 * n)},((2 * n) \ n):] by E, F, ZFMISC_1:def 2;
hence [(2 * n),m] in the InternalRel of (Mycielskian R) by D, U5; :: thesis: verum