let R be symmetric irreflexive RelStr ; ( card the carrier of R = 2 & the carrier of R in FinSETS implies RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp )
assume that
A1:
card the carrier of R = 2
and
A2:
the carrier of R in FinSETS
; RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp
consider a, b being object such that
A3:
the carrier of R = {a,b}
and
A4:
( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} )
by A1, Th6;
set A = {a};
set B = {b};
A5:
{a} c= the carrier of R
A6:
{b} c= the carrier of R
then reconsider B = {b} as Subset of R ;
reconsider A = {a} as Subset of R by A5;
set H1 = subrelstr A;
set H2 = subrelstr B;
reconsider H2 = subrelstr B as non empty strict symmetric irreflexive RelStr by YELLOW_0:def 15;
A7:
the carrier of H2 = B
by YELLOW_0:def 15;
then
the InternalRel of H2 c= [:{b},{b}:]
;
then
the InternalRel of H2 c= {[b,b]}
by ZFMISC_1:29;
then A8:
( the InternalRel of H2 = {} or the InternalRel of H2 = {[b,b]} )
by ZFMISC_1:33;
A9:
the InternalRel of H2 = {}
the carrier of H2 c= the carrier of R
by A6, YELLOW_0:def 15;
then
the carrier of H2 in FinSETS
by A2, CLASSES1:3, CLASSES2:def 2;
then A11:
H2 in fin_RelStr_sp
by A7, NECKLA_2:def 5;
reconsider H1 = subrelstr A as non empty strict symmetric irreflexive RelStr by YELLOW_0:def 15;
A12:
the carrier of H1 = A
by YELLOW_0:def 15;
then A13:
the carrier of R = the carrier of H1 \/ the carrier of H2
by A3, A7, ENUMSET1:1;
a <> b
then A14:
A misses B
by ZFMISC_1:11;
then A15:
the carrier of H1 misses the carrier of H2
by A7, YELLOW_0:def 15;
the InternalRel of H1 c= [:{a},{a}:]
by A12;
then
the InternalRel of H1 c= {[a,a]}
by ZFMISC_1:29;
then A16:
( the InternalRel of H1 = {} or the InternalRel of H1 = {[a,a]} )
by ZFMISC_1:33;
A17:
the InternalRel of H1 = {}
the carrier of H1 c= the carrier of R
by A5, YELLOW_0:def 15;
then
the carrier of H1 in FinSETS
by A2, CLASSES1:3, CLASSES2:def 2;
then A19:
H1 in fin_RelStr_sp
by A12, NECKLA_2:def 5;
per cases
( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} )
by A4;
suppose A20:
the
InternalRel of
R = {[a,b],[b,a]}
;
RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp set S =
sum_of (
H1,
H2);
the
InternalRel of
(sum_of (H1,H2)) = (( the InternalRel of H1 \/ the InternalRel of H2) \/ [:A,B:]) \/ [:B,A:]
by A12, A7, NECKLA_2:def 3;
then
the
InternalRel of
(sum_of (H1,H2)) = {[a,b]} \/ [:{b},{a}:]
by A17, A9, ZFMISC_1:29;
then
the
InternalRel of
(sum_of (H1,H2)) = {[a,b]} \/ {[b,a]}
by ZFMISC_1:29;
then A21:
the
InternalRel of
(sum_of (H1,H2)) = the
InternalRel of
R
by A20, ENUMSET1:1;
the
carrier of
(sum_of (H1,H2)) = the
carrier of
R
by A13, NECKLA_2:def 3;
hence
RelStr(# the
carrier of
R, the
InternalRel of
R #)
in fin_RelStr_sp
by A12, A19, A7, A11, A14, A21, NECKLA_2:def 5;
verum end; suppose A22:
the
InternalRel of
R = {}
;
RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp set U =
union_of (
H1,
H2);
( the
InternalRel of
(union_of (H1,H2)) = the
InternalRel of
H1 \/ the
InternalRel of
H2 & the
carrier of
(union_of (H1,H2)) = the
carrier of
R )
by A13, NECKLA_2:def 2;
hence
RelStr(# the
carrier of
R, the
InternalRel of
R #)
in fin_RelStr_sp
by A19, A11, A15, A17, A9, A22, NECKLA_2:def 5;
verum end;