let n be Nat; :: thesis: for R being NatRelStr of n holds the InternalRel of R c= the InternalRel of (Mycielskian R)
let R be NatRelStr of n; :: thesis: the InternalRel of R c= the InternalRel of (Mycielskian R)
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
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;
hence the InternalRel of R c= the InternalRel of (Mycielskian R) by Th3; :: thesis: verum