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 ;
set A = {a};
set B = {b};
A5: {a} c= the carrier of R
proof
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 ; :: thesis: verum
end;
A6: {b} c= the carrier of R
proof
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 ; :: thesis: verum
end;
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 = {}
proof end;
the carrier of H2 c= the carrier of R by ;
then the carrier of H2 in FinSETS by ;
then A11: H2 in fin_RelStr_sp by ;
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 ;
a <> b
proof
assume not a <> b ; :: thesis: contradiction
then the carrier of R = {a} by ;
hence contradiction by A1, CARD_1:30; :: thesis: verum
end;
then A14: A misses B by ZFMISC_1:11;
then A15: the carrier of H1 misses the carrier of H2 by ;
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 end;
the carrier of H1 c= the carrier of R by ;
then the carrier of H1 in FinSETS by ;
then A19: H1 in fin_RelStr_sp by ;
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]} ; :: 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 ;
then the InternalRel of (sum_of (H1,H2)) = {[a,b]} \/ [:{b},{a}:] by ;
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 ;
the carrier of (sum_of (H1,H2)) = the carrier of R by ;
hence RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp by ; :: thesis: verum
end;
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 ;
hence RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp by ; :: thesis: verum
end;
end;