let G be irreflexive RelStr ; :: thesis: ( G in fin_RelStr_sp implies ComplRelStr G in fin_RelStr_sp )
assume A1: G in fin_RelStr_sp ; :: thesis: ComplRelStr G in fin_RelStr_sp
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 ;
A2: 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 A3: 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
A4: card the carrier of G = k and
A5: G in fin_RelStr_sp ; :: thesis: ComplRelStr G in fin_RelStr_sp

per cases ( G is non empty trivial 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 A5, NECKLA_2:6;

suppose G is non empty trivial strict RelStr ; :: thesis: ComplRelStr G in fin_RelStr_sp

hence ComplRelStr G in fin_RelStr_sp by A5, 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
A6: ( the carrier of G1 misses the carrier of G2 & G1 in fin_RelStr_sp & G2 in fin_RelStr_sp ) and
A7: ( G = union_of G1,G2 or G = sum_of G1,G2 ) ;
A8: ( not G1 is empty & G1 is finite ) by A6, NECKLA_2:4;
then ( not the carrier of G1 is empty & the carrier of G1 is finite ) ;
then reconsider n1 = card the carrier of G1 as Nat ;
A11: ( not G2 is empty & G2 is finite ) by A6, NECKLA_2:4;
then ( not the carrier of G2 is empty & the carrier of G2 is finite ) ;
then reconsider n2 = card the carrier of G2 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 A7;

suppose A14: G = union_of G1,G2 ; :: thesis: ComplRelStr G in fin_RelStr_sp

then reconsider G1 = G1 as irreflexive RelStr by Th9;
reconsider G2 = G2 as irreflexive RelStr by A14, Th9;
A15: the carrier of G = the carrier of G1 \/ the carrier of G2 by A14, NECKLA_2:def 2;
reconsider cG1 = the carrier of G1 as non empty finite set by A8;
reconsider cG2 = the carrier of G2 as non empty finite set by A11;
A16: card the carrier of G = (card cG1) + (card cG2) by A6, A15, CARD_2:53;
card cG1 = n1 ;
then n1 <> 0 ;
then A17: n1 > 0 ;
card cG2 = n2 ;
then n2 <> 0 ;
then A18: n2 > 0 ;
n1 < k

proof

assume not n1 < k ; :: thesis: contradiction
then k + 0 < n2 + n1 by A18, XREAL_1:10;
hence contradiction by A4, A16; :: thesis: verum

end;

then A19: ComplRelStr G1 in fin_RelStr_sp by A3, A6;
n2 < k

proof

assume not n2 < k ; :: thesis: contradiction
then k + 0 < n1 + n2 by A17, XREAL_1:10;
hence contradiction by A4, A16; :: thesis: verum

end;

then A20: ComplRelStr G2 in fin_RelStr_sp by A3, A6;
A21: ComplRelStr G = sum_of (ComplRelStr G1),(ComplRelStr G2) by A6, A14, Th17;
( the carrier of (ComplRelStr G1) = the carrier of G1 & the carrier of (ComplRelStr G2) = the carrier of G2 ) by NECKLACE:def 9;
hence ComplRelStr G in fin_RelStr_sp by A6, A19, A20, A21, NECKLA_2:def 5; :: thesis: verum

end;

suppose A22: G = sum_of G1,G2 ; :: thesis: ComplRelStr G in fin_RelStr_sp

then reconsider G1 = G1 as irreflexive RelStr by Th9;
reconsider G2 = G2 as irreflexive RelStr by A22, Th9;
A23: the carrier of G = the carrier of G1 \/ the carrier of G2 by A22, NECKLA_2:def 3;
reconsider cG1 = the carrier of G1 as non empty finite set by A8;
reconsider cG2 = the carrier of G2 as non empty finite set by A11;
A24: card the carrier of G = (card cG1) + (card cG2) by A6, A23, CARD_2:53;
card cG1 = n1 ;
then n1 <> 0 ;
then A25: n1 > 0 ;
card cG2 = n2 ;
then n2 <> 0 ;
then A26: n2 > 0 ;
n1 < k

proof

assume not n1 < k ; :: thesis: contradiction
then k + 0 < n2 + n1 by A26, XREAL_1:10;
hence contradiction by A4, A24; :: thesis: verum

end;

then A27: ComplRelStr G1 in fin_RelStr_sp by A3, A6;
n2 < k

proof

assume not n2 < k ; :: thesis: contradiction
then k + 0 < n1 + n2 by A25, XREAL_1:10;
hence contradiction by A4, A24; :: thesis: verum

end;

then A28: ComplRelStr G2 in fin_RelStr_sp by A3, A6;
A29: ComplRelStr G = union_of (ComplRelStr G1),(ComplRelStr G2) by A6, A22, Th18;
( the carrier of (ComplRelStr G1) = the carrier of G1 & the carrier of (ComplRelStr G2) = the carrier of G2 ) by NECKLACE:def 9;
hence ComplRelStr G in fin_RelStr_sp by A6, A27, A28, A29, NECKLA_2:def 5; :: thesis: verum

end;

end;

end;

end;

end;

end;

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