defpred S2[ Nat] means Mycielskian n is irreflexive ;
A1:
S2[ 0 ]
by Th49;
A2:
for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
set cMRn = the
carrier of
(Mycielskian n);
set iMRn = the
InternalRel of
(Mycielskian n);
set cMRn1 = the
carrier of
(Mycielskian (n + 1));
set iMRn1 = the
InternalRel of
(Mycielskian (n + 1));
assume A3:
S2[
n]
;
S2[n + 1]
assume
not
S2[
n + 1]
;
contradiction
then consider x being
set such that A4:
x in the
carrier of
(Mycielskian (n + 1))
and A5:
[x,x] in the
InternalRel of
(Mycielskian (n + 1))
by NECKLACE:def 5;
A6:
Mycielskian (n + 1) = Mycielskian (Mycielskian n)
by Th49;
set N =
(3 * (2 |^ n)) -' 1;
A7:
the
carrier of
(Mycielskian (n + 1)) = (2 * ((3 * (2 |^ n)) -' 1)) + 1
by A6, Def7;
A8:
the
carrier of
(Mycielskian n) = (3 * (2 |^ n)) -' 1
by Def7;
x in Segm ((2 * ((3 * (2 |^ n)) -' 1)) + 1)
by A7, A4;
then reconsider x =
x as
Nat ;
( (
x < (3 * (2 |^ n)) -' 1 &
x < (3 * (2 |^ n)) -' 1 ) or (
x < (3 * (2 |^ n)) -' 1 &
(3 * (2 |^ n)) -' 1
<= x &
x < 2
* ((3 * (2 |^ n)) -' 1) ) or (
(3 * (2 |^ n)) -' 1
<= x &
x < 2
* ((3 * (2 |^ n)) -' 1) &
x < (3 * (2 |^ n)) -' 1 ) or (
x = 2
* ((3 * (2 |^ n)) -' 1) &
(3 * (2 |^ n)) -' 1
<= x &
x < 2
* ((3 * (2 |^ n)) -' 1) ) or (
(3 * (2 |^ n)) -' 1
<= x &
x < 2
* ((3 * (2 |^ n)) -' 1) &
x = 2
* ((3 * (2 |^ n)) -' 1) ) )
by A6, A5, Th38;
then A9:
x in Segm ((3 * (2 |^ n)) -' 1)
by NAT_1:44;
then
[x,x] in the
InternalRel of
(Mycielskian n)
by A5, A6, Th40;
hence
contradiction
by A3, A8, A9, NECKLACE:def 5;
verum
end;
for n being Nat holds S2[n]
from NAT_1:sch 2(A1, A2);
hence
Mycielskian n is irreflexive
; verum