let n be Nat; for R being NatRelStr of n
for x, y being Nat st [x,y] in the InternalRel of R holds
( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )
let R be NatRelStr of n; for x, y being Nat st [x,y] in the InternalRel of R holds
( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )
let a, b be Nat; ( [a,b] in the InternalRel of R implies ( [a,(b + n)] in the InternalRel of (Mycielskian R) & [(a + n),b] in the InternalRel of (Mycielskian R) ) )
assume A1:
[a,b] in the InternalRel of R
; ( [a,(b + n)] in the InternalRel of (Mycielskian R) & [(a + n),b] in the InternalRel of (Mycielskian R) )
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
A2:
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;
reconsider ap1 = a, bp1 = b as Element of NAT by ORDINAL1:def 12;
[ap1,(bp1 + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R }
by A1;
hence
[a,(b + n)] in the InternalRel of (Mycielskian R)
by A2, Th4; [(a + n),b] in the InternalRel of (Mycielskian R)
[(ap1 + n),bp1] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R }
by A1;
hence
[(a + n),b] in the InternalRel of (Mycielskian R)
by A2, Th4; verum