defpred S1[ Nat] means for G being irreflexive RelStr st card the carrier of G = \$1 & G in fin_RelStr_sp holds
ComplRelStr G in fin_RelStr_sp ;
let G be irreflexive RelStr ; :: thesis: ( G in fin_RelStr_sp implies ComplRelStr G in fin_RelStr_sp )
A1: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )

assume A2: for n being Nat st n < k holds
S1[n] ; :: thesis: S1[k]
let G be irreflexive RelStr ; :: thesis: ( card the carrier of G = k & G in fin_RelStr_sp implies ComplRelStr G in fin_RelStr_sp )
assume that
A3: card the carrier of G = k and
A4: G in fin_RelStr_sp ; :: thesis:
per cases ( G is 1 -element strict RelStr or ex G1, G2 being strict RelStr st
( the carrier of G1 misses the carrier of G2 & G1 in fin_RelStr_sp & G2 in fin_RelStr_sp & ( G = union_of (G1,G2) or G = sum_of (G1,G2) ) ) )
by ;
suppose ex G1, G2 being strict RelStr st
( the carrier of G1 misses the carrier of G2 & G1 in fin_RelStr_sp & G2 in fin_RelStr_sp & ( G = union_of (G1,G2) or G = sum_of (G1,G2) ) ) ; :: thesis:
then consider G1, G2 being strict RelStr such that
A5: the carrier of G1 misses the carrier of G2 and
A6: G1 in fin_RelStr_sp and
A7: G2 in fin_RelStr_sp and
A8: ( G = union_of (G1,G2) or G = sum_of (G1,G2) ) ;
A9: ( not G2 is empty & G2 is finite ) by ;
then reconsider n2 = card the carrier of G2 as Nat ;
A10: ( not G1 is empty & G1 is finite ) by ;
then reconsider n1 = card the carrier of G1 as Nat ;
thus ComplRelStr G in fin_RelStr_sp :: thesis: verum
proof
per cases ( G = union_of (G1,G2) or G = sum_of (G1,G2) ) by A8;
suppose A11: G = union_of (G1,G2) ; :: thesis:
then reconsider G2 = G2 as irreflexive RelStr by Th9;
reconsider G1 = G1 as irreflexive RelStr by ;
reconsider cG1 = the carrier of G1 as non empty finite set by A10;
reconsider cG2 = the carrier of G2 as non empty finite set by A9;
the carrier of G = the carrier of G1 \/ the carrier of G2 by ;
then A12: card the carrier of G = (card cG1) + (card cG2) by ;
A13: card cG1 = n1 ;
n2 < k
proof
assume not n2 < k ; :: thesis: contradiction
then k + 0 < n1 + n2 by ;
hence contradiction by A3, A12; :: thesis: verum
end;
then A14: ComplRelStr G2 in fin_RelStr_sp by A2, A7;
A15: ( the carrier of () = the carrier of G1 & the carrier of () = the carrier of G2 ) by NECKLACE:def 8;
A16: card cG2 = n2 ;
n1 < k
proof
assume not n1 < k ; :: thesis: contradiction
then k + 0 < n2 + n1 by ;
hence contradiction by A3, A12; :: thesis: verum
end;
then A17: ComplRelStr G1 in fin_RelStr_sp by A2, A6;
ComplRelStr G = sum_of ((),()) by ;
hence ComplRelStr G in fin_RelStr_sp by ; :: thesis: verum
end;
suppose A18: G = sum_of (G1,G2) ; :: thesis:
then reconsider G2 = G2 as irreflexive RelStr by Th9;
reconsider G1 = G1 as irreflexive RelStr by ;
reconsider cG1 = the carrier of G1 as non empty finite set by A10;
reconsider cG2 = the carrier of G2 as non empty finite set by A9;
the carrier of G = the carrier of G1 \/ the carrier of G2 by ;
then A19: card the carrier of G = (card cG1) + (card cG2) by ;
A20: card cG1 = n1 ;
n2 < k
proof
assume not n2 < k ; :: thesis: contradiction
then k + 0 < n1 + n2 by ;
hence contradiction by A3, A19; :: thesis: verum
end;
then A21: ComplRelStr G2 in fin_RelStr_sp by A2, A7;
A22: ( the carrier of () = the carrier of G1 & the carrier of () = the carrier of G2 ) by NECKLACE:def 8;
A23: card cG2 = n2 ;
n1 < k
proof
assume not n1 < k ; :: thesis: contradiction
then k + 0 < n2 + n1 by ;
hence contradiction by A3, A19; :: thesis: verum
end;
then A24: ComplRelStr G1 in fin_RelStr_sp by A2, A6;
ComplRelStr G = union_of ((),()) by ;
hence ComplRelStr G in fin_RelStr_sp by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
A25: for k being Nat holds S1[k] from assume A26: G in fin_RelStr_sp ; :: thesis:
then G is finite by NECKLA_2:4;
then card the carrier of G is Nat ;
hence ComplRelStr G in fin_RelStr_sp by ; :: thesis: verum