let X be RelStr ; ( X in fin_RelStr_sp implies X is symmetric )
assume A1:
X in fin_RelStr_sp
; X is symmetric
per cases
( X is trivial or not X is trivial )
;
suppose A2:
X is
trivial
;
X is symmetric thus
X is
symmetric
verumproof
per cases
( the carrier of X is empty or ex x being object st the carrier of X = {x} )
by A2, ZFMISC_1:131;
suppose
ex
x being
object st the
carrier of
X = {x}
;
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
verumproof
per cases
( the InternalRel of X = {} or the InternalRel of X = {[x,x]} )
by A6, ZFMISC_1:33;
suppose A9:
the
InternalRel of
X = {[x,x]}
;
X is symmetric let a,
b be
object ;
NECKLACE:def 3,
RELAT_2:def 3 ( 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
;
[b,a] in the InternalRel of XA11:
[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;
verum end;
end; end;
end; end; suppose A12:
not
X is
trivial
;
X is symmetric defpred S1[
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
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A16:
S1[
k]
;
S1[k + 1]
reconsider k1 =
k as
Element of
NAT by ORDINAL1:def 12;
let Y be non
empty RelStr ;
( 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
;
( 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
;
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; A35:
S1[
0 ]
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A35, A15);
hence
X is
symmetric
by A1, A12, A14;
verum end;