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 )

defpred S_{1}[ 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

S_{1}[k] ) holds

S_{1}[n]
_{1}[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; :: thesis: verum

defpred S

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

S

S

proof

A47:
for k being Nat holds S
let n be Nat; :: thesis: ( ( for k being Nat st k < n holds

S_{1}[k] ) implies S_{1}[n] )

assume A2: for k being Nat st k < n holds

S_{1}[k]
; :: thesis: S_{1}[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 that

A3: G is N-free and

A4: card the carrier of G = n and

A5: the carrier of G in FinSETS ; :: thesis: RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp

end;S

assume A2: for k being Nat st k < n holds

S

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 that

A3: G is N-free and

A4: card the carrier of G = n and

A5: 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 ) )
;

end;

suppose
G is trivial
; :: thesis: RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp

then
the carrier of G is 1 -element
;

then reconsider G = G as 1 -element RelStr by STRUCT_0:def 19;

RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp by A5, NECKLA_2:def 5;

hence RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp ; :: thesis: verum

end;then reconsider G = G as 1 -element RelStr by STRUCT_0:def 19;

RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp by A5, NECKLA_2:def 5;

hence RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp ; :: thesis: verum

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

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; :: thesis: verum

end;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; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

suppose A26:
( 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 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 :: thesis: verum

end;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 :: thesis: verum

proof
end;

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;

end;

( 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 A33:
R is trivial RelStr
; :: thesis: RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp

not the carrier of R is empty
;

then A34: not A is empty by YELLOW_0:def 15;

A is trivial by A33, YELLOW_0:def 15;

then consider a being object such that

A35: A = {a} by A34, ZFMISC_1:131;

A36: the carrier of G \/ {x} = the carrier of G

then ( the carrier of G = {a,x} & a <> x ) by A26, A36, ENUMSET1:1;

then card the carrier of G = 2 by CARD_2:57;

hence RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp by A5, Th33; :: thesis: verum

end;then A34: not A is empty by YELLOW_0:def 15;

A is trivial by A33, YELLOW_0:def 15;

then consider a being object such that

A35: A = {a} by A34, ZFMISC_1:131;

A36: the carrier of G \/ {x} = the carrier of G

proof

{a} \/ {x} = the carrier of G \/ {x}
by A35, XBOOLE_1:39;
thus
the carrier of G \/ {x} c= the carrier of G
:: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= the carrier of G \/ {x}

assume c in the carrier of G ; :: thesis: c in the carrier of G \/ {x}

hence c in the carrier of G \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;proof

let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in the carrier of G or c in the carrier of G \/ {x} )
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in the carrier of G \/ {x} or c in the carrier of G )

assume c in the carrier of G \/ {x} ; :: thesis: c in the carrier of G

then ( c in the carrier of G or c in {x} ) by XBOOLE_0:def 3;

hence c in the carrier of G ; :: thesis: verum

end;assume c in the carrier of G \/ {x} ; :: thesis: c in the carrier of G

then ( c in the carrier of G or c in {x} ) by XBOOLE_0:def 3;

hence c in the carrier of G ; :: thesis: verum

assume c in the carrier of G ; :: thesis: c in the carrier of G \/ {x}

hence c in the carrier of G \/ {x} by XBOOLE_0:def 3; :: thesis: verum

then ( the carrier of G = {a,x} & a <> x ) by A26, A36, ENUMSET1:1;

then card the carrier of G = 2 by CARD_2:57;

hence RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp by A5, Th33; :: thesis: verum

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

( 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

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 :: thesis: verum

end;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 :: thesis: verum

proof
end;

per cases
( R = union_of (R1,R2) or R = sum_of (R1,R2) )
by A40;

end;

suppose A41:
R = union_of (R1,R2)
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

suppose A42:
R = sum_of (R1,R2)
; :: thesis: RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp

not ComplRelStr R2 is empty

not ComplRelStr R1 is empty

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; :: thesis: verum

end;proof

then reconsider R22 = ComplRelStr R2 as non empty RelStr ;
assume
ComplRelStr R2 is empty
; :: thesis: contradiction

then R2 is empty ;

hence contradiction by A39, NECKLA_2:4; :: thesis: verum

end;then R2 is empty ;

hence contradiction by A39, NECKLA_2:4; :: thesis: verum

not ComplRelStr R1 is empty

proof

then reconsider R11 = ComplRelStr R1 as non empty RelStr ;
assume
ComplRelStr R1 is empty
; :: thesis: contradiction

then R1 is empty ;

hence contradiction by A38, NECKLA_2:4; :: thesis: verum

end;then R1 is empty ;

hence contradiction by A38, NECKLA_2:4; :: thesis: verum

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; :: thesis: verum

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; :: thesis: verum