let R be symmetric irreflexive RelStr ; :: thesis: ( card the carrier of R = 2 implies ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) )
assume A1: card the carrier of R = 2 ; :: thesis: ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )
then reconsider X = the carrier of R as finite set ;
consider a, b being set such that
A2: ( a <> b & X = {a,b} ) by A1, CARD_2:79;
set Q = the InternalRel of R;
A3: the InternalRel of R c= {[a,b],[b,a]}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of R or x in {[a,b],[b,a]} )
assume A4: x in the InternalRel of R ; :: thesis: x in {[a,b],[b,a]}
then consider x1, x2 being set such that
A5: ( x = [x1,x2] & x1 in X & x2 in X ) by RELSET_1:6;
A6: ( ( x1 = a or x1 = b ) & ( x2 = a or x2 = b ) ) by A2, A5, TARSKI:def 2;

per cases ( x = [a,a] or x = [a,b] or x = [b,a] or x = [b,b] ) by A5, A6;

suppose A7: x = [a,a] ; :: thesis: x in {[a,b],[b,a]}

a in the carrier of R by A2, TARSKI:def 2;
hence x in {[a,b],[b,a]} by A4, A7, NECKLACE:def 6; :: thesis: verum

end;

suppose x = [a,b] ; :: thesis: x in {[a,b],[b,a]}

hence x in {[a,b],[b,a]} by TARSKI:def 2; :: thesis: verum

end;

suppose x = [b,a] ; :: thesis: x in {[a,b],[b,a]}

hence x in {[a,b],[b,a]} by TARSKI:def 2; :: thesis: verum

end;

suppose A8: x = [b,b] ; :: thesis: x in {[a,b],[b,a]}

b in the carrier of R by A2, TARSKI:def 2;
hence x in {[a,b],[b,a]} by A4, A8, NECKLACE:def 6; :: thesis: verum

end;

end;

end;

per cases ( the InternalRel of R = {} or the InternalRel of R = {[a,b]} or the InternalRel of R = {[b,a]} or the InternalRel of R = {[a,b],[b,a]} ) by A3, ZFMISC_1:42;

suppose the InternalRel of R = {} ; :: thesis: ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )

hence ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) by A2; :: thesis: verum

end;

suppose A9: the InternalRel of R = {[a,b]} ; :: thesis: ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )

then A10: [a,b] in the InternalRel of R by TARSKI:def 1;
A11: ( a in X & b in X ) by A2, TARSKI:def 2;
the InternalRel of R is_symmetric_in X by NECKLACE:def 4;
then [b,a] in the InternalRel of R by A10, A11, RELAT_2:def 3;
then [b,a] = [a,b] by A9, TARSKI:def 1;
hence ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) by A2, ZFMISC_1:33; :: thesis: verum

end;

suppose A12: the InternalRel of R = {[b,a]} ; :: thesis: ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )

then A13: [b,a] in the InternalRel of R by TARSKI:def 1;
A14: ( a in X & b in X ) by A2, TARSKI:def 2;
the InternalRel of R is_symmetric_in X by NECKLACE:def 4;
then [a,b] in the InternalRel of R by A13, A14, RELAT_2:def 3;
then [b,a] = [a,b] by A12, TARSKI:def 1;
hence ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) by A2, ZFMISC_1:33; :: thesis: verum

end;

suppose the InternalRel of R = {[a,b],[b,a]} ; :: thesis: ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )

hence ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) by A2; :: thesis: verum

end;

end;