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 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 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 ) ) ;
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 ;
hence RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp ; :: thesis: verum
end;
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 ;
then A9: card the carrier of G1 in Segm (card cR) by ;
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 ;
G2 is full SubRelStr of G by A6, A7, Th10;
then A12: G2 is N-free by ;
the carrier of G2 in FinSETS by ;
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 ;
reconsider cG1 = the carrier of G1 as finite set by A9;
A15: card cG1 < card cR by ;
the carrier of G1 in FinSETS by ;
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 ; :: 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 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 ;
then A19: card the carrier of G1 in Segm (card cR) by ;
then reconsider G1 = G1 as non empty finite strict symmetric irreflexive RelStr ;
A20: card the carrier of G2 in Segm (card cR) by ;
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 ;
G2 is full SubRelStr of G by ;
then A22: G2 is N-free by ;
the carrier of G2 in FinSETS by ;
then A23: G2 in fin_RelStr_sp by A2, A4, A21, A22;
G1 is full SubRelStr of G by ;
then A24: G1 is N-free by ;
reconsider cG1 = the carrier of G1 as finite set by A19;
A25: card cG1 < card cR by ;
the carrier of G1 in FinSETS by ;
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 ; :: thesis: verum
end;
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 ;
A29: the carrier of R c= the carrier of G by ;
card A = (card the carrier of G) - () by CARD_2:44;
then A30: card A = n - 1 by ;
n - 1 < (n - 1) + 1 by XREAL_1:29;
then A31: card the carrier of R < n by ;
R is N-free by ;
then A32: R in fin_RelStr_sp by ;
thus RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp :: thesis: verum
proof
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 ;
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 ;
then consider a being object such that
A35: A = {a} by ;
A36: the carrier of G \/ {x} = the carrier of G
proof
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}
proof
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;
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} )
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;
{a} \/ {x} = the carrier of G \/ {x} by ;
then ( the carrier of G = {a,x} & a <> x ) by ;
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 ; :: thesis: verum
end;
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
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
per cases ( R = union_of (R1,R2) or R = sum_of (R1,R2) ) by A40;
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 ;
then reconsider R2 = R2 as non empty SubRelStr of G by ;
R1 is SubRelStr of R by ;
then reconsider R1 = R1 as non empty SubRelStr of G by ;
subrelstr (([#] G) \ {x}) = union_of (R1,R2) by A41;
then G embeds Necklace 4 by ;
hence RelStr(# the carrier of G, the InternalRel of G #) in fin_RelStr_sp by ; :: thesis: verum
end;
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 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 ;
A46: ( ComplRelStr G9 is path-connected & not G9 is trivial ) by ;
ComplRelStr R = union_of ((),()) by ;
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 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
A47: for k being Nat holds S1[k] from 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