let n be Nat; :: thesis:
let R be NatRelStr of n; :: thesis:
let a, b be Nat; :: thesis:
set cR = the carrier of R;
set iR = the InternalRel of R;
defpred S₂[] means [a,b] in the InternalRel of (Mycielskian R);
defpred S₃[] means ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) );
A1: 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;
assume A2: S₂[] ; :: thesis:

per cases in the InternalRel of R or [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in [:{(2 * n)},((2 * n) \ n):] or [a,b] in [:((2 * n) \ n),{(2 * n)}:] ) by A2, A1, Th4;

suppose [a,b] in the InternalRel of R ; :: thesis:

then ( a in the carrier of R & b in the carrier of R ) by ZFMISC_1:87;
then ( a in Segm n & b in Segm n ) by Def7;
hence S₃[] by NAT_1:44; :: thesis:

end;

suppose [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; :: thesis:

then consider x, y being Element of NAT such that
A3: [x,(y + n)] = [a,b] and
A4: [x,y] in the InternalRel of R ;
y in the carrier of R by A4, ZFMISC_1:87;
then y in Segm n by Def7;
then y < n by NAT_1:44;
then A5: y + n < n + n by XREAL_1:6;
x in the carrier of R by A4, ZFMISC_1:87;
then x in Segm n by Def7;
then x < n by NAT_1:44;
hence S₃[] by A5, A3, XTUPLE_0:1; :: thesis:

end;

suppose [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; :: thesis:

then consider x, y being Element of NAT such that
A6: [(x + n),y] = [a,b] and
A7: [x,y] in the InternalRel of R ;
x in the carrier of R by A7, ZFMISC_1:87;
then x in Segm n by Def7;
then x < n by NAT_1:44;
then A8: x + n < n + n by XREAL_1:6;
y in the carrier of R by A7, ZFMISC_1:87;
then y in Segm n by Def7;
then y < n by NAT_1:44;
hence S₃[] by A8, A6, XTUPLE_0:1; :: thesis:

end;

suppose A9: [a,b] in [:{(2 * n)},((2 * n) \ n):] ; :: thesis:

A10: b in (Segm (2 * n)) \ (Segm n) by A9, ZFMISC_1:87;
a in {(2 * n)} by A9, ZFMISC_1:87;
hence S₃[] by A10, Th2, TARSKI:def 1; :: thesis:

end;

suppose A11: [a,b] in [:((2 * n) \ n),{(2 * n)}:] ; :: thesis:

A12: a in (Segm (2 * n)) \ (Segm n) by A11, ZFMISC_1:87;
b in {(2 * n)} by A11, ZFMISC_1:87;
hence S₃[] by A12, Th2, TARSKI:def 1; :: thesis:

end;

end;