defpred S_{1}[ 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_{1}[n] ) holds

S_{1}[k]
_{1}[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

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

S

proof

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

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

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

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

end;S

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

S

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;

end;

( 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
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

( 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

end;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
end;

per cases
( G = union_of (G1,G2) or G = sum_of (G1,G2) )
by A8;

end;

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

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

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;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

then A14:
ComplRelStr G2 in fin_RelStr_sp
by A2, A7;
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 k + 0 < n1 + n2 by A13, XREAL_1:8;

hence contradiction by A3, A12; :: thesis: verum

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

then A17:
ComplRelStr G1 in fin_RelStr_sp
by A2, A6;
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 k + 0 < n2 + n1 by A16, XREAL_1:8;

hence contradiction by A3, A12; :: thesis: verum

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

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

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

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;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

then A21:
ComplRelStr G2 in fin_RelStr_sp
by A2, A7;
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 k + 0 < n1 + n2 by A20, XREAL_1:8;

hence contradiction by A3, A19; :: thesis: verum

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

then A24:
ComplRelStr G1 in fin_RelStr_sp
by A2, A6;
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 k + 0 < n2 + n1 by A23, XREAL_1:8;

hence contradiction by A3, A19; :: thesis: verum

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

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