let R be non empty finite strict symmetric irreflexive RelStr ; ( R is N-free & the carrier of R in FinSETS implies RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp )
defpred S1[ Nat] means for G being non empty finite strict symmetric irreflexive RelStr st G is N-free & card the carrier of G = $1 & the carrier of G in FinSETS holds
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp ;
A1:
for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be
Nat;
( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A2:
for
k being
Nat st
k < n holds
S1[
k]
;
S1[n]
let G be non
empty finite strict symmetric irreflexive RelStr ;
( G is N-free & card the carrier of G = n & the carrier of G in FinSETS implies RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp )
set CG =
ComplRelStr G;
assume that A3:
G is
N-free
and A4:
card the
carrier of
G = n
and A5:
the
carrier of
G in FinSETS
;
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp
per cases
( G is trivial or ( not G is path-connected & not G is trivial ) or ( not ComplRelStr G is path-connected & not G is trivial ) or ( not G is trivial & G is path-connected & ComplRelStr G is path-connected ) )
;
suppose
( not
G is
path-connected & not
G is
trivial )
;
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp then consider G1,
G2 being non
empty strict symmetric irreflexive RelStr such that A6:
the
carrier of
G1 misses the
carrier of
G2
and A7:
RelStr(# the
carrier of
G, the
InternalRel of
G #)
= union_of (
G1,
G2)
by Th30;
set cG1 = the
carrier of
G1;
set cG2 = the
carrier of
G2;
set R =
RelStr(# the
carrier of
G, the
InternalRel of
G #);
set cR = the
carrier of
RelStr(# the
carrier of
G, the
InternalRel of
G #);
reconsider cR = the
carrier of
RelStr(# the
carrier of
G, the
InternalRel of
G #) as
finite set ;
A8:
cR = the
carrier of
G1 \/ the
carrier of
G2
by A7, NECKLA_2:def 2;
then A9:
card the
carrier of
G1 in Segm (card cR)
by A6, Lm1;
then reconsider G1 =
G1 as non
empty finite strict symmetric irreflexive RelStr ;
reconsider cR =
cR as
finite set ;
A10:
card the
carrier of
G2 in Segm (card cR)
by A6, A8, Lm1;
then reconsider G2 =
G2 as non
empty finite strict symmetric irreflexive RelStr ;
reconsider cG2 = the
carrier of
G2 as
finite set by A10;
A11:
card cG2 < card cR
by A10, NAT_1:44;
G2 is
full SubRelStr of
G
by A6, A7, Th10;
then A12:
G2 is
N-free
by A3, Th23;
the
carrier of
G2 in FinSETS
by A5, A8, CLASSES1:3, CLASSES2:def 2, XBOOLE_1:7;
then A13:
G2 in fin_RelStr_sp
by A2, A4, A11, A12;
G1 is
full SubRelStr of
G
by A6, A7, Th10;
then A14:
G1 is
N-free
by A3, Th23;
reconsider cG1 = the
carrier of
G1 as
finite set by A9;
A15:
card cG1 < card cR
by A9, NAT_1:44;
the
carrier of
G1 in FinSETS
by A5, A8, CLASSES1:3, CLASSES2:def 2, XBOOLE_1:7;
then
G1 in fin_RelStr_sp
by A2, A4, A15, A14;
hence
RelStr(# the
carrier of
G, the
InternalRel of
G #)
in fin_RelStr_sp
by A6, A7, A13, NECKLA_2:def 5;
verum end; suppose
( not
ComplRelStr G is
path-connected & not
G is
trivial )
;
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp then consider G1,
G2 being non
empty strict symmetric irreflexive RelStr such that A16:
the
carrier of
G1 misses the
carrier of
G2
and A17:
RelStr(# the
carrier of
G, the
InternalRel of
G #)
= sum_of (
G1,
G2)
by Th31;
set cG1 = the
carrier of
G1;
set cG2 = the
carrier of
G2;
set R =
RelStr(# the
carrier of
G, the
InternalRel of
G #);
set cR = the
carrier of
RelStr(# the
carrier of
G, the
InternalRel of
G #);
reconsider cR = the
carrier of
RelStr(# the
carrier of
G, the
InternalRel of
G #) as
finite set ;
A18:
cR = the
carrier of
G1 \/ the
carrier of
G2
by A17, NECKLA_2:def 3;
then A19:
card the
carrier of
G1 in Segm (card cR)
by A16, Lm1;
then reconsider G1 =
G1 as non
empty finite strict symmetric irreflexive RelStr ;
A20:
card the
carrier of
G2 in Segm (card cR)
by A16, A18, Lm1;
then reconsider G2 =
G2 as non
empty finite strict symmetric irreflexive RelStr ;
reconsider cG2 = the
carrier of
G2 as
finite set by A20;
A21:
card cG2 < card cR
by A20, NAT_1:44;
G2 is
full SubRelStr of
G
by A16, A17, Th10;
then A22:
G2 is
N-free
by A3, Th23;
the
carrier of
G2 in FinSETS
by A5, A18, CLASSES1:3, CLASSES2:def 2, XBOOLE_1:7;
then A23:
G2 in fin_RelStr_sp
by A2, A4, A21, A22;
G1 is
full SubRelStr of
G
by A16, A17, Th10;
then A24:
G1 is
N-free
by A3, Th23;
reconsider cG1 = the
carrier of
G1 as
finite set by A19;
A25:
card cG1 < card cR
by A19, NAT_1:44;
the
carrier of
G1 in FinSETS
by A5, A18, CLASSES1:3, CLASSES2:def 2, XBOOLE_1:7;
then
G1 in fin_RelStr_sp
by A2, A4, A25, A24;
hence
RelStr(# the
carrier of
G, the
InternalRel of
G #)
in fin_RelStr_sp
by A16, A17, A23, NECKLA_2:def 5;
verum end; suppose A26:
( not
G is
trivial &
G is
path-connected &
ComplRelStr G is
path-connected )
;
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp consider x being
object such that A27:
x in the
carrier of
G
by XBOOLE_0:def 1;
reconsider x =
x as
Element of
G by A27;
set A = the
carrier of
G \ {x};
A28:
the
carrier of
G \ {x} c= the
carrier of
G
;
reconsider A = the
carrier of
G \ {x} as
Subset of
G ;
set R =
subrelstr A;
reconsider R =
subrelstr A as non
empty finite symmetric irreflexive RelStr by A26, YELLOW_0:def 15;
A29:
the
carrier of
R c= the
carrier of
G
by A28, YELLOW_0:def 15;
card A = (card the carrier of G) - (card {x})
by CARD_2:44;
then A30:
card A = n - 1
by A4, CARD_2:42;
n - 1
< (n - 1) + 1
by XREAL_1:29;
then A31:
card the
carrier of
R < n
by A30, YELLOW_0:def 15;
R is
N-free
by A3, Th23;
then A32:
R in fin_RelStr_sp
by A2, A5, A31, A29, CLASSES1:3, CLASSES2:def 2;
thus
RelStr(# the
carrier of
G, the
InternalRel of
G #)
in fin_RelStr_sp
verumproof
per cases
( R is trivial RelStr or ex R1, R2 being strict RelStr st
( the carrier of R1 misses the carrier of R2 & R1 in fin_RelStr_sp & R2 in fin_RelStr_sp & ( R = union_of (R1,R2) or R = sum_of (R1,R2) ) ) )
by A32, NECKLA_2:6;
suppose
ex
R1,
R2 being
strict RelStr st
( the
carrier of
R1 misses the
carrier of
R2 &
R1 in fin_RelStr_sp &
R2 in fin_RelStr_sp & (
R = union_of (
R1,
R2) or
R = sum_of (
R1,
R2) ) )
;
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp then consider R1,
R2 being
strict RelStr such that A37:
the
carrier of
R1 misses the
carrier of
R2
and A38:
R1 in fin_RelStr_sp
and A39:
R2 in fin_RelStr_sp
and A40:
(
R = union_of (
R1,
R2) or
R = sum_of (
R1,
R2) )
;
thus
RelStr(# the
carrier of
G, the
InternalRel of
G #)
in fin_RelStr_sp
verumproof
per cases
( R = union_of (R1,R2) or R = sum_of (R1,R2) )
by A40;
suppose A41:
R = union_of (
R1,
R2)
;
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp
R2 is
SubRelStr of
R
by A37, A40, Th10;
then reconsider R2 =
R2 as non
empty SubRelStr of
G by A39, NECKLA_2:4, YELLOW_6:7;
R1 is
SubRelStr of
R
by A37, A40, Th10;
then reconsider R1 =
R1 as non
empty SubRelStr of
G by A38, NECKLA_2:4, YELLOW_6:7;
subrelstr (([#] G) \ {x}) = union_of (
R1,
R2)
by A41;
then
G embeds Necklace 4
by A26, A37, Th39;
hence
RelStr(# the
carrier of
G, the
InternalRel of
G #)
in fin_RelStr_sp
by A3, NECKLA_2:def 1;
verum end; suppose A42:
R = sum_of (
R1,
R2)
;
RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp
not
ComplRelStr R2 is
empty
then reconsider R22 =
ComplRelStr R2 as non
empty RelStr ;
not
ComplRelStr R1 is
empty
then reconsider R11 =
ComplRelStr R1 as non
empty RelStr ;
reconsider G9 =
ComplRelStr G as non
empty symmetric irreflexive RelStr ;
reconsider x9 =
x as
Element of
G9 by NECKLACE:def 8;
A43:
( the
carrier of
R11 = the
carrier of
R1 & the
carrier of
R22 = the
carrier of
R2 )
by NECKLACE:def 8;
A44:
ComplRelStr R =
ComplRelStr (subrelstr (([#] G) \ {x}))
.=
subrelstr (([#] G9) \ {x9})
by Th20
;
A45:
G9 is
N-free
by A3, Th25;
A46:
(
ComplRelStr G9 is
path-connected & not
G9 is
trivial )
by A26, Th16, NECKLACE:def 8;
ComplRelStr R = union_of (
(ComplRelStr R1),
(ComplRelStr R2))
by A37, A42, Th18;
then
G9 embeds Necklace 4
by A26, A37, A43, A46, A44, Th39;
hence
RelStr(# the
carrier of
G, the
InternalRel of
G #)
in fin_RelStr_sp
by A45, NECKLA_2:def 1;
verum
end; end;
end; end;
end;
A47:
for k being Nat holds S1[k]
from NAT_1:sch 4(A1);
card the carrier of R is Nat
;
hence
( R is N-free & the carrier of R in FinSETS implies RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp )
by A47; verum