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
per cases
( X is trivial or not X is trivial )
;
suppose
X is
trivial
;
:: thesis: X is symmetric then A2:
the
carrier of
X is
trivial
;
thus
X is
symmetric
:: thesis: verumproof
per cases
( the carrier of X is empty or ex x being set st the carrier of X = {x} )
by A2, REALSET1:def 4;
suppose
ex
x being
set st the
carrier of
X = {x}
;
:: thesis: X is symmetric then consider x being
set such that A4:
the
carrier of
X = {x}
;
A5:
[:the carrier of X,the carrier of X:] = {[x,x]}
by A4, ZFMISC_1:35;
thus
X is
symmetric
:: thesis: verumproof
per cases
( the InternalRel of X = {} or the InternalRel of X = {[x,x]} )
by A5, ZFMISC_1:39;
suppose A7:
the
InternalRel of
X = {[x,x]}
;
:: thesis: X is symmetric let a,
b be
set ;
:: according to NECKLACE:def 4,
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 A8:
(
a in the
carrier of
X &
b in the
carrier of
X &
[a,b] in the
InternalRel of
X )
;
:: thesis: [b,a] in the InternalRel of Xthen
[a,b] = [x,x]
by A7, TARSKI:def 1;
then
(
a = x &
b = x )
by ZFMISC_1:33;
hence
[b,a] in the
InternalRel of
X
by A8;
:: thesis: verum end;
end; end;
end; end; suppose A9:
not
X is
trivial
;
:: thesis: 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 ;
A10:
S1[
0 ]
;
A14:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A15:
S1[
k]
;
:: thesis: S1[k + 1]
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 A16:
( not
Y is
trivial &
Y in fin_RelStr_sp )
;
:: thesis: ( not card the carrier of Y c= k + 1 or Y is symmetric )
reconsider k1 =
k as
Element of
NAT by ORDINAL1:def 13;
set cY = the
carrier of
Y;
consider R being
strict RelStr such that A17:
(
Y = R & the
carrier of
R in FinSETS )
by A16, NECKLA_2:def 4;
reconsider cY = the
carrier of
Y as
finite set by A17;
consider H1,
H2 being
strict RelStr such that A18:
( the
carrier of
H1 misses the
carrier of
H2 &
H1 in fin_RelStr_sp &
H2 in fin_RelStr_sp )
and A19:
(
Y = union_of H1,
H2 or
Y = sum_of H1,
H2 )
by A16, NECKLA_2:6;
set cH1 = the
carrier of
H1;
set cH2 = the
carrier of
H2;
A20:
card cY = card (the carrier of H1 \/ the carrier of H2)
by A19, NECKLA_2:def 2, NECKLA_2:def 3;
consider R1 being
strict RelStr such that A21:
(
H1 = R1 & the
carrier of
R1 in FinSETS )
by A18, NECKLA_2:def 4;
reconsider cH1 = the
carrier of
H1 as
finite set by A21;
consider R2 being
strict RelStr such that A22:
(
H2 = R2 & the
carrier of
R2 in FinSETS )
by A18, NECKLA_2:def 4;
reconsider cH2 = the
carrier of
H2 as
finite set by A22;
A23:
card cY = (card cH1) + (card cH2)
by A18, A20, CARD_2:53;
assume
card the
carrier of
Y c= k + 1
;
:: thesis: Y is symmetric
then
card cY c= card (k1 + 1)
by CARD_1:def 5;
then
card cY <= card (k1 + 1)
by NAT_1:40;
then A24:
card cY <= k + 1
by CARD_1:def 5;
( not
H1 is
empty & not
H2 is
empty )
by A18, NECKLA_2:4;
then
( not
cH1 is
empty & not
cH2 is
empty )
;
then
(
card cH1 <> 0 &
card cH2 <> 0 )
;
then A25:
(
card cH1 >= 1 &
card cH2 >= 1 )
by NAT_1:14;
end; A39:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A10, A14);
consider R being
strict RelStr such that A40:
(
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;
the
carrier of
X is
finite
by A40;
then
card the
carrier of
X is
Nat
;
hence
X is
symmetric
by A1, A9, A39;
:: thesis: verum end;