let n be Nat; :: thesis: for R being NatRelStr of n holds the carrier of R c= the carrier of (Mycielskian R)
let R be NatRelStr of n; :: thesis: the carrier of R c= the carrier of (Mycielskian R)
A: the carrier of R = n by LNRS;
n <= n + n by NAT_1:12;
then n <= (2 * n) + 1 by NAT_1:12;
then n c= (2 * n) + 1 by NAT_1:40;
hence the carrier of R c= the carrier of (Mycielskian R) by A, LNRS; :: thesis: verum