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)
A1: the carrier of R = n by Def7;
n <= n + n by NAT_1:12;
then n <= (2 * n) + 1 by NAT_1:12;
then Segm n c= Segm ((2 * n) + 1) by NAT_1:39;
hence the carrier of R c= the carrier of (Mycielskian R) by A1, Def7; :: thesis: verum