let X be RelStr ; :: thesis: ( X in fin_RelStr_sp implies X is symmetric )

assume A1: X in fin_RelStr_sp ; :: thesis: X is symmetric

assume A1: X in fin_RelStr_sp ; :: thesis: X is symmetric

per cases
( X is trivial or not X is trivial )
;

end;

suppose A2:
X is trivial
; :: thesis: X is symmetric

thus
X is symmetric
:: thesis: verum

end;proof
end;

per cases
( the carrier of X is empty or ex x being object st the carrier of X = {x} )
by A2, ZFMISC_1:131;

end;

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

let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis: ( not a in the carrier of X or not b in the carrier of X or not [a,b] in the InternalRel of X or [b,a] in the InternalRel of X )

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: [b,a] in the InternalRel of X

thus [b,a] in the InternalRel of X by A3, A4; :: thesis: verum

end;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: [b,a] in the InternalRel of X

thus [b,a] in the InternalRel of X by A3, A4; :: thesis: verum

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

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: verum

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

proof
end;

per cases
( the InternalRel of X = {} or the InternalRel of X = {[x,x]} )
by A6, ZFMISC_1:33;

end;

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

let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis: ( not a in the carrier of X or not b in the carrier of X or not [a,b] in the InternalRel of X or [b,a] in the InternalRel of X )

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: [b,a] in the InternalRel of X

thus [b,a] in the InternalRel of X by A7, A8; :: thesis: verum

end;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: [b,a] in the InternalRel of X

thus [b,a] in the InternalRel of X by A7, A8; :: thesis: verum

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

let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis: ( not a in the carrier of X or not b in the carrier of X or not [a,b] in the InternalRel of X or [b,a] in the InternalRel of X )

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: [b,a] in the InternalRel of X

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: verum

end;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: [b,a] in the InternalRel of X

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: verum

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

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

S_{1}[k + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A35, A15);

hence X is symmetric by A1, A12, A14; :: thesis: verum

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

S

proof

A35:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A16: S_{1}[k]
; :: thesis: S_{1}[k + 1]

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

let Y be non empty RelStr ; :: thesis: ( not Y is trivial & Y in fin_RelStr_sp & card the carrier of Y c= k + 1 implies Y is symmetric )

assume that

A17: not Y is trivial and

A18: Y in fin_RelStr_sp ; :: thesis: ( not card the carrier of Y c= k + 1 or Y is symmetric )

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: Y is symmetric

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;

end;assume A16: S

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

let Y be non empty RelStr ; :: thesis: ( not Y is trivial & Y in fin_RelStr_sp & card the carrier of Y c= k + 1 implies Y is symmetric )

assume that

A17: not Y is trivial and

A18: Y in fin_RelStr_sp ; :: thesis: ( not card the carrier of Y c= k + 1 or Y is symmetric )

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: Y is symmetric

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
( card cY <= k or ( card cY = k + 1 & k = 0 ) or ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 = 1 & card cH2 = 1 ) or ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 = 1 & card cH2 > 1 ) or ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 > 1 & card cH2 = 1 ) or ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 > 1 & card cH2 > 1 ) )
by A25, A23, A26, A27, NAT_1:8, XXREAL_0:1;

end;

suppose
card cY <= k
; :: thesis: Y is symmetric

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: verum

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

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

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: verum

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

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

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: verum

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

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

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: verum

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

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

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: verum

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

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

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

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

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: verum

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

proof

then
card cH2 <= k
by NAT_1:13;
assume
not card cH2 < k + 1
; :: thesis: contradiction

then (card cH1) + (card cH2) >= (k + 1) + 1 by A26, XREAL_1:7;

hence contradiction by A32, NAT_1:13; :: thesis: verum

end;then (card cH1) + (card cH2) >= (k + 1) + 1 by A26, XREAL_1:7;

hence contradiction by A32, NAT_1:13; :: thesis: verum

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

proof

then
card cH1 <= k
by NAT_1:13;
assume
not card cH1 < k + 1
; :: thesis: contradiction

then (card cH1) + (card cH2) >= (k + 1) + 1 by A27, XREAL_1:7;

hence contradiction by A32, NAT_1:13; :: thesis: verum

end;then (card cH1) + (card cH2) >= (k + 1) + 1 by A27, XREAL_1:7;

hence contradiction by A32, NAT_1:13; :: thesis: verum

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: verum

for k being Nat holds S

hence X is symmetric by A1, A12, A14; :: thesis: verum