let R be symmetric irreflexive RelStr ; :: thesis: ( 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 ; :: thesis: 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

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 = {}

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 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 = {}

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;

assume that

A1: card the carrier of R = 2 and

A2: the carrier of R in FinSETS ; :: thesis: 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

proof

A6:
{b} c= the carrier of R
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a} or x in the carrier of R )

assume x in {a} ; :: thesis: x in the carrier of R

then x = a by TARSKI:def 1;

hence x in the carrier of R by A3, TARSKI:def 2; :: thesis: verum

end;assume x in {a} ; :: thesis: x in the carrier of R

then x = a by TARSKI:def 1;

hence x in the carrier of R by A3, TARSKI:def 2; :: thesis: verum

proof

then reconsider B = {b} as Subset of R ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {b} or x in the carrier of R )

assume x in {b} ; :: thesis: x in the carrier of R

then x = b by TARSKI:def 1;

hence x in the carrier of R by A3, TARSKI:def 2; :: thesis: verum

end;assume x in {b} ; :: thesis: x in the carrier of R

then x = b by TARSKI:def 1;

hence x in the carrier of R by A3, TARSKI:def 2; :: thesis: verum

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 = {}

proof

the carrier of H2 c= the carrier of R
by A6, YELLOW_0:def 15;
b in B
by TARSKI:def 1;

then b in the carrier of H2 by YELLOW_0:def 15;

then A10: not [b,b] in the InternalRel of H2 by NECKLACE:def 5;

assume not the InternalRel of H2 = {} ; :: thesis: contradiction

hence contradiction by A8, A10, TARSKI:def 1; :: thesis: verum

end;then b in the carrier of H2 by YELLOW_0:def 15;

then A10: not [b,b] in the InternalRel of H2 by NECKLACE:def 5;

assume not the InternalRel of H2 = {} ; :: thesis: contradiction

hence contradiction by A8, A10, TARSKI:def 1; :: thesis: verum

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

proof

then A14:
A misses B
by ZFMISC_1:11;
assume
not a <> b
; :: thesis: contradiction

then the carrier of R = {a} by A3, ENUMSET1:29;

hence contradiction by A1, CARD_1:30; :: thesis: verum

end;then the carrier of R = {a} by A3, ENUMSET1:29;

hence contradiction by A1, CARD_1:30; :: thesis: verum

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 = {}

proof

the carrier of H1 c= the carrier of R
by A5, YELLOW_0:def 15;
a in A
by TARSKI:def 1;

then a in the carrier of H1 by YELLOW_0:def 15;

then A18: not [a,a] in the InternalRel of H1 by NECKLACE:def 5;

assume not the InternalRel of H1 = {} ; :: thesis: contradiction

hence contradiction by A16, A18, TARSKI:def 1; :: thesis: verum

end;then a in the carrier of H1 by YELLOW_0:def 15;

then A18: not [a,a] in the InternalRel of H1 by NECKLACE:def 5;

assume not the InternalRel of H1 = {} ; :: thesis: contradiction

hence contradiction by A16, A18, TARSKI:def 1; :: thesis: verum

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;

end;

suppose A20:
the InternalRel of R = {[a,b],[b,a]}
; :: thesis: 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; :: thesis: verum

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

suppose A22:
the InternalRel of R = {}
; :: thesis: 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; :: thesis: verum

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