let X be RelStr ; :: thesis:
assume A1: X in fin_RelStr_sp ; :: thesis:

suppose A2: X is trivial ; :: thesis:

thus X is symmetric :: thesis:

per cases by A2, ZFMISC_1:131;

suppose A3: the carrier of X is empty ; :: thesis:

let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis:
assume that
A4: a in the carrier of X and
b in the carrier of X and
[a,b] in the InternalRel of X ; :: thesis:
thus [b,a] in the InternalRel of X by A3, A4; :: thesis:

end;

suppose ex x being object st the carrier of X = {x} ; :: thesis:

then consider x being object such that
A5: the carrier of X = {x} ;
A6: [: the carrier of X, the carrier of X:] = {[x,x]} by A5, ZFMISC_1:29;
thus X is symmetric :: thesis:

per cases by A6, ZFMISC_1:33;

suppose A7: the InternalRel of X = {} ; :: thesis:

let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis:
assume that
a in the carrier of X and
b in the carrier of X and
A8: [a,b] in the InternalRel of X ; :: thesis:
thus [b,a] in the InternalRel of X by A7, A8; :: thesis:

end;

suppose A9: the InternalRel of X = {[x,x]} ; :: thesis:

let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis:
assume that
a in the carrier of X and
b in the carrier of X and
A10: [a,b] in the InternalRel of X ; :: thesis:
A11: [a,b] = [x,x] by A9, A10, TARSKI:def 1;
then a = x by XTUPLE_0:1;
hence [b,a] in the InternalRel of X by A10, A11, XTUPLE_0:1; :: thesis:

end;

end;

end;

end;

end;

end;

end;

suppose A12: not X is trivial ; :: thesis:

defpred S₁[ Nat] means for X being non empty RelStr st not X is trivial & X in fin_RelStr_sp & card the carrier of X c= $1 holds
X is symmetric ;
A13: ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) by A1, NECKLA_2:def 4;
reconsider X = X as non empty RelStr by A1, NECKLA_2:4;
A14: card the carrier of X is Nat by A13;
A15: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A16: S₁[k] ; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
let Y be non empty RelStr ; :: thesis:
assume that
A17: not Y is trivial and
A18: Y in fin_RelStr_sp ; :: thesis:
consider H1, H2 being strict RelStr such that
A19: the carrier of H1 misses the carrier of H2 and
A20: H1 in fin_RelStr_sp and
A21: H2 in fin_RelStr_sp and
A22: ( Y = union_of (H1,H2) or Y = sum_of (H1,H2) ) by A17, A18, NECKLA_2:6;
ex R being strict RelStr st
( Y = R & the carrier of R in FinSETS ) by A18, NECKLA_2:def 4;
then reconsider cY = the carrier of Y as finite set ;
assume card the carrier of Y c= k + 1 ; :: thesis:
then Segm (card cY) c= Segm (card (k1 + 1)) ;
then card cY <= card (k1 + 1) by NAT_1:39;
then A23: card cY <= k + 1 ;
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
A24: card cY = card ( the carrier of H1 \/ the carrier of H2) by A22, NECKLA_2:def 2, NECKLA_2:def 3;
ex R2 being strict RelStr st
( H2 = R2 & the carrier of R2 in FinSETS ) by A21, NECKLA_2:def 4;
then reconsider cH2 = the carrier of H2 as finite set ;
ex R1 being strict RelStr st
( H1 = R1 & the carrier of R1 in FinSETS ) by A20, NECKLA_2:def 4;
then reconsider cH1 = the carrier of H1 as finite set ;
A25: card cY = (card cH1) + (card cH2) by A19, A24, CARD_2:40;
not H1 is empty by A20, NECKLA_2:4;
then A26: card cH1 >= 1 by NAT_1:14;
not H2 is empty by A21, NECKLA_2:4;
then A27: card cH2 >= 1 by NAT_1:14;

per cases by A25, A23, A26, A27, NAT_1:8, XXREAL_0:1;

suppose card cY <= k ; :: thesis:

then card cY <= card k1 ;
then Segm (card cY) c= Segm (card k) by NAT_1:39;
then card the carrier of Y c= k1 ;
hence Y is symmetric by A16, A17, A18; :: thesis:

end;

suppose A28: ( card cY = k + 1 & k = 0 ) ; :: thesis:

set x = the set ;
card cY = card { the set } by A28, CARD_1:30;
then cY,{ the set } are_equipotent by CARD_1:5;
then ex y being object st cY = {y} by CARD_1:28;
hence Y is symmetric by A17; :: thesis:

end;

suppose A29: ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 = 1 & card cH2 = 1 ) ; :: thesis:

then ex x being object st cH1 = {x} by CARD_2:42;
then the InternalRel of H1 is_symmetric_in cH1 by Th5;
then reconsider H1 = H1 as symmetric RelStr by NECKLACE:def 3;
ex y being object st cH2 = {y} by A29, CARD_2:42;
then the InternalRel of H2 is_symmetric_in cH2 by Th5;
then reconsider H2 = H2 as symmetric RelStr by NECKLACE:def 3;
union_of (H1,H2) is symmetric ;
hence Y is symmetric by A22; :: thesis:

end;

suppose A30: ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 = 1 & card cH2 > 1 ) ; :: thesis:

then ex x being object st cH1 = {x} by CARD_2:42;
then the InternalRel of H1 is_symmetric_in cH1 by Th5;
then reconsider H1 = H1 as symmetric RelStr by NECKLACE:def 3;
not card cH2 is trivial by A30, NAT_2:28;
then card cH2 >= 2 by NAT_2:29;
then ( not H2 is empty & not H2 is trivial ) by NAT_D:60;
then reconsider H2 = H2 as symmetric RelStr by A16, A21, A30;
union_of (H1,H2) is symmetric ;
hence Y is symmetric by A22; :: thesis:

end;

suppose A31: ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 > 1 & card cH2 = 1 ) ; :: thesis:

then ex x being object st cH2 = {x} by CARD_2:42;
then the InternalRel of H2 is_symmetric_in cH2 by Th5;
then reconsider H2 = H2 as symmetric RelStr by NECKLACE:def 3;
not card cH1 is trivial by A31, NAT_2:28;
then card cH1 >= 2 by NAT_2:29;
then ( not H1 is empty & not H1 is trivial ) by NAT_D:60;
then reconsider H1 = H1 as symmetric RelStr by A16, A20, A31;
union_of (H1,H2) is symmetric ;
hence Y is symmetric by A22; :: thesis:

end;

suppose A32: ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 > 1 & card cH2 > 1 ) ; :: thesis:

then not card cH2 is trivial by NAT_2:28;
then card cH2 >= 2 by NAT_2:29;
then A33: ( not H2 is empty & not H2 is trivial ) by NAT_D:60;
card cH2 < k + 1

assume not card cH2 < k + 1 ; :: thesis:
then (card cH1) + (card cH2) >= (k + 1) + 1 by A26, XREAL_1:7;
hence contradiction by A32, NAT_1:13; :: thesis:

end;

then card cH2 <= k by NAT_1:13;
then card cH2 <= card k1 ;
then Segm (card cH2) c= Segm (card k) by NAT_1:39;
then card cH2 c= k1 ;
then reconsider H2 = H2 as symmetric RelStr by A16, A21, A33;
not card cH1 is trivial by A32, NAT_2:28;
then card cH1 >= 2 by NAT_2:29;
then A34: ( not H1 is empty & not H1 is trivial ) by NAT_D:60;
card cH1 < k + 1

assume not card cH1 < k + 1 ; :: thesis:
then (card cH1) + (card cH2) >= (k + 1) + 1 by A27, XREAL_1:7;
hence contradiction by A32, NAT_1:13; :: thesis:

end;

then card cH1 <= k by NAT_1:13;
then card cH1 <= card k1 ;
then Segm (card cH1) c= Segm (card k) by NAT_1:39;
then card cH1 c= k1 ;
then reconsider H1 = H1 as symmetric RelStr by A16, A20, A34;
union_of (H1,H2) is symmetric ;
hence Y is symmetric by A22; :: thesis:

end;

end;

end;

A35: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A35, A15);
hence X is symmetric by A1, A12, A14; :: thesis:

end;

end;