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;
:: thesis: ( ( 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]
;
:: thesis: S1[n]
let G be non
empty finite strict symmetric irreflexive RelStr ;
:: thesis: ( 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 A3:
(
G is
N-free &
card the
carrier of
G = n & the
carrier of
G in FinSETS )
;
:: thesis: 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 )
;
:: thesis: 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 A4:
the
carrier of
G1 misses the
carrier of
G2
and A5:
RelStr(# the
carrier of
G,the
InternalRel of
G #)
= union_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 #);
A6:
the
carrier of
RelStr(# the
carrier of
G,the
InternalRel of
G #)
= the
carrier of
G1 \/ the
carrier of
G2
by A5, NECKLA_2:def 2;
then A7:
card the
carrier of
G1 in card the
carrier of
RelStr(# the
carrier of
G,the
InternalRel of
G #)
by A4, Lm1;
then A8:
the
carrier of
G1 is
finite
by CARD_2:68;
reconsider cG1 = the
carrier of
G1 as
finite set by A7, CARD_2:68;
reconsider G1 =
G1 as non
empty finite strict symmetric irreflexive RelStr by A8;
reconsider cR = the
carrier of
RelStr(# the
carrier of
G,the
InternalRel of
G #) as
finite set ;
A9:
card cG1 < card cR
by A7, NAT_1:45;
G1 is
full SubRelStr of
G
by A4, A5, Th10;
then A10:
G1 is
N-free
by A3, Th23;
the
carrier of
G1 in FinSETS
by A3, A6, CLASSES1:6, CLASSES2:def 2, XBOOLE_1:7;
then A11:
G1 in fin_RelStr_sp
by A2, A3, A9, A10;
A12:
card the
carrier of
G2 in card cR
by A4, A6, Lm1;
then A13:
the
carrier of
G2 is
finite
by CARD_2:68;
reconsider cG2 = the
carrier of
G2 as
finite set by A12, CARD_2:68;
reconsider G2 =
G2 as non
empty finite strict symmetric irreflexive RelStr by A13;
A14:
card cG2 < card cR
by A12, NAT_1:45;
G2 is
full SubRelStr of
G
by A4, A5, Th10;
then A15:
G2 is
N-free
by A3, Th23;
the
carrier of
G2 in FinSETS
by A3, A6, CLASSES1:6, CLASSES2:def 2, XBOOLE_1:7;
then
G2 in fin_RelStr_sp
by A2, A3, A14, A15;
hence
RelStr(# the
carrier of
G,the
InternalRel of
G #)
in fin_RelStr_sp
by A4, A5, A11, NECKLA_2:def 5;
:: thesis: verum end; suppose
( not
ComplRelStr G is
path-connected & not
G is
trivial )
;
:: thesis: 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 Th32;
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 #);
A18:
the
carrier of
RelStr(# the
carrier of
G,the
InternalRel of
G #)
= the
carrier of
G1 \/ the
carrier of
G2
by A17, NECKLA_2:def 3;
then A19:
card the
carrier of
G1 in card the
carrier of
RelStr(# the
carrier of
G,the
InternalRel of
G #)
by A16, Lm1;
then A20:
the
carrier of
G1 is
finite
by CARD_2:68;
reconsider cG1 = the
carrier of
G1 as
finite set by A19, CARD_2:68;
reconsider G1 =
G1 as non
empty finite strict symmetric irreflexive RelStr by A20;
reconsider cR = the
carrier of
RelStr(# the
carrier of
G,the
InternalRel of
G #) as
finite set ;
A21:
card cG1 < card cR
by A19, NAT_1:45;
G1 is
full SubRelStr of
G
by A16, A17, Th10;
then A22:
G1 is
N-free
by A3, Th23;
the
carrier of
G1 in FinSETS
by A3, A18, CLASSES1:6, CLASSES2:def 2, XBOOLE_1:7;
then A23:
G1 in fin_RelStr_sp
by A2, A3, A21, A22;
A24:
card the
carrier of
G2 in card cR
by A16, A18, Lm1;
then A25:
the
carrier of
G2 is
finite
by CARD_2:68;
reconsider cG2 = the
carrier of
G2 as
finite set by A24, CARD_2:68;
reconsider G2 =
G2 as non
empty finite strict symmetric irreflexive RelStr by A25;
A26:
card cG2 < card cR
by A24, NAT_1:45;
G2 is
full SubRelStr of
G
by A16, A17, Th10;
then A27:
G2 is
N-free
by A3, Th23;
the
carrier of
G2 in FinSETS
by A3, A18, CLASSES1:6, CLASSES2:def 2, XBOOLE_1:7;
then
G2 in fin_RelStr_sp
by A2, A3, A26, A27;
hence
RelStr(# the
carrier of
G,the
InternalRel of
G #)
in fin_RelStr_sp
by A16, A17, A23, NECKLA_2:def 5;
:: thesis: verum end; suppose A28:
( not
G is
trivial &
G is
path-connected &
ComplRelStr G is
path-connected )
;
:: thesis: RelStr(# the carrier of G,the InternalRel of G #) in fin_RelStr_sp consider x being
set such that A29:
x in the
carrier of
G
by XBOOLE_0:def 1;
reconsider x =
x as
Element of
G by A29;
set A = the
carrier of
G \ {x};
A30:
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;
not
subrelstr A is
empty
by A28, YELLOW_0:def 15;
then reconsider R =
subrelstr A as non
empty finite symmetric irreflexive RelStr ;
A31:
card the
carrier of
R < n
A33:
R is
N-free
by A3, Th23;
the
carrier of
R in FinSETS
then A34:
R in fin_RelStr_sp
by A2, A31, A33;
thus
RelStr(# the
carrier of
G,the
InternalRel of
G #)
in fin_RelStr_sp
:: thesis: 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 A34, 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 ) )
;
:: thesis: RelStr(# the carrier of G,the InternalRel of G #) in fin_RelStr_sp then consider R1,
R2 being
strict RelStr such that A40:
the
carrier of
R1 misses the
carrier of
R2
and A41:
(
R1 in fin_RelStr_sp &
R2 in fin_RelStr_sp & (
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
:: thesis: verumproof
per cases
( R = union_of R1,R2 or R = sum_of R1,R2 )
by A41;
suppose A42:
R = union_of R1,
R2
;
:: thesis: RelStr(# the carrier of G,the InternalRel of G #) in fin_RelStr_sp
R1 is
SubRelStr of
R
by A40, A41, Th10;
then reconsider R1 =
R1 as non
empty SubRelStr of
G by A41, NECKLA_2:4, YELLOW_6:16;
R2 is
SubRelStr of
R
by A40, A41, Th10;
then reconsider R2 =
R2 as non
empty SubRelStr of
G by A41, NECKLA_2:4, YELLOW_6:16;
subrelstr (([#] G) \ {x}) = union_of R1,
R2
by A42;
then
G embeds Necklace 4
by A28, A40, Th40;
hence
RelStr(# the
carrier of
G,the
InternalRel of
G #)
in fin_RelStr_sp
by A3, NECKLA_2:def 1;
:: thesis: verum end; suppose
R = sum_of R1,
R2
;
:: thesis: RelStr(# the carrier of G,the InternalRel of G #) in fin_RelStr_sp then A43:
ComplRelStr R = union_of (ComplRelStr R1),
(ComplRelStr R2)
by A40, Th18;
reconsider G' =
ComplRelStr G as non
empty symmetric irreflexive RelStr ;
A44:
not
ComplRelStr R1 is
empty
A45:
not
ComplRelStr R2 is
empty
reconsider R11 =
ComplRelStr R1 as non
empty RelStr by A44;
reconsider R22 =
ComplRelStr R2 as non
empty RelStr by A45;
reconsider x' =
x as
Element of
G' by NECKLACE:def 9;
A46:
( the
carrier of
R11 = the
carrier of
R1 & the
carrier of
R22 = the
carrier of
R2 )
by NECKLACE:def 9;
A47:
(
G' is
path-connected &
ComplRelStr G' is
path-connected )
by A28, Th16;
A48:
not
G' is
trivial
by A28, NECKLACE:def 9;
ComplRelStr R =
ComplRelStr (subrelstr (([#] G) \ {x}))
.=
subrelstr (([#] G') \ {x'})
by Th20
;
then A50:
G' embeds Necklace 4
by A40, A43, A46, A47, A48, Th40;
G' is
N-free
by A3, Th25;
hence
RelStr(# the
carrier of
G,the
InternalRel of
G #)
in fin_RelStr_sp
by A50, NECKLA_2:def 1;
:: thesis: verum end;
end; end;
end; end;
end;
A51:
for k being Nat holds S1[k]
from NAT_1:sch 4(A1);
let R be non empty finite strict symmetric irreflexive RelStr ; :: thesis: ( R is N-free & the carrier of R in FinSETS implies RelStr(# the carrier of R,the InternalRel of R #) in fin_RelStr_sp )
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 A51; :: thesis: verum