defpred S₁[ 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
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A2: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[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: ComplRelStr G in fin_RelStr_sp

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 A4, NECKLA_2:6;

suppose G is 1 -element strict RelStr ; :: thesis: ComplRelStr G in fin_RelStr_sp

hence ComplRelStr G in fin_RelStr_sp by A4, Th15; :: thesis: verum

end;

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: ComplRelStr G in fin_RelStr_sp

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 A7, NECKLA_2:4;
then reconsider n2 = card the carrier of G2 as Nat ;
A10: ( not G1 is empty & G1 is finite ) by A6, NECKLA_2:4;
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: ComplRelStr G in fin_RelStr_sp

then reconsider G2 = G2 as irreflexive RelStr by Th9;
reconsider G1 = G1 as irreflexive RelStr by A11, Th9;
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 A11, NECKLA_2:def 2;
then A12: card the carrier of G = (card cG1) + (card cG2) by A5, CARD_2:40;
A13: card cG1 = n1 ;
n2 < k

proof

assume not n2 < k ; :: thesis: contradiction
then k + 0 < n1 + n2 by A13, XREAL_1:8;
hence contradiction by A3, A12; :: thesis: verum

end;

then A14: ComplRelStr G2 in fin_RelStr_sp by A2, A7;
A15: ( the carrier of (ComplRelStr G1) = the carrier of G1 & the carrier of (ComplRelStr G2) = 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 A16, XREAL_1:8;
hence contradiction by A3, A12; :: thesis: verum

end;

then A17: ComplRelStr G1 in fin_RelStr_sp by A2, A6;
ComplRelStr G = sum_of ((ComplRelStr G1),(ComplRelStr G2)) by A5, A11, Th17;
hence ComplRelStr G in fin_RelStr_sp by A5, A17, A14, A15, NECKLA_2:def 5; :: thesis: verum

end;

suppose A18: G = sum_of (G1,G2) ; :: thesis: ComplRelStr G in fin_RelStr_sp

then reconsider G2 = G2 as irreflexive RelStr by Th9;
reconsider G1 = G1 as irreflexive RelStr by A18, Th9;
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 A18, NECKLA_2:def 3;
then A19: card the carrier of G = (card cG1) + (card cG2) by A5, CARD_2:40;
A20: card cG1 = n1 ;
n2 < k

proof

assume not n2 < k ; :: thesis: contradiction
then k + 0 < n1 + n2 by A20, XREAL_1:8;
hence contradiction by A3, A19; :: thesis: verum

end;

then A21: ComplRelStr G2 in fin_RelStr_sp by A2, A7;
A22: ( the carrier of (ComplRelStr G1) = the carrier of G1 & the carrier of (ComplRelStr G2) = 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 A23, XREAL_1:8;
hence contradiction by A3, A19; :: thesis: verum

end;

then A24: ComplRelStr G1 in fin_RelStr_sp by A2, A6;
ComplRelStr G = union_of ((ComplRelStr G1),(ComplRelStr G2)) by A5, A18, Th18;
hence ComplRelStr G in fin_RelStr_sp by A5, A24, A21, A22, NECKLA_2:def 5; :: thesis: verum

end;

end;

end;

end;

end;

end;

A25: for k being Nat holds S₁[k] from NAT_1:sch 4(A1);
assume A26: G in fin_RelStr_sp ; :: thesis: ComplRelStr G in fin_RelStr_sp
then G is finite by NECKLA_2:4;
then card the carrier of G is Nat ;
hence ComplRelStr G in fin_RelStr_sp by A26, A25; :: thesis: verum