let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( [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 ; :: thesis: ( [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; :: thesis: [(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; :: thesis: verum