let R be symmetric irreflexive RelStr ; :: thesis: ( card the carrier of R = 2 implies ex a, b being object st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) )
set Q = the InternalRel of R;
assume A1: card the carrier of R = 2 ; :: thesis: ex a, b being object 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 object such that
A2: a <> b and
A3: X = {a,b} by A1, CARD_2:60;
A4: the InternalRel of R c= {[a,b],[b,a]}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of R or x in {[a,b],[b,a]} )
assume A5: x in the InternalRel of R ; :: thesis: x in {[a,b],[b,a]}
then consider x1, x2 being object such that
A6: x = [x1,x2] and
A7: x1 in X and
A8: x2 in X by RELSET_1:2;
A9: ( x1 = a or x1 = b ) by A3, A7, TARSKI:def 2;

per cases ( x = [a,a] or x = [a,b] or x = [b,a] or x = [b,b] ) by A3, A6, A8, A9, TARSKI:def 2;

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

a in the carrier of R by A3, TARSKI:def 2;
hence x in {[a,b],[b,a]} by A5, A10, NECKLACE:def 5; :: 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 A11: x = [b,b] ; :: thesis: x in {[a,b],[b,a]}

b in the carrier of R by A3, TARSKI:def 2;
hence x in {[a,b],[b,a]} by A5, A11, NECKLACE:def 5; :: 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 A4, ZFMISC_1:36;

suppose the InternalRel of R = {} ; :: thesis: ex a, b being object 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 object st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) by A3; :: thesis: verum

end;

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

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

end;

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

A16: ( a in X & b in X ) by A3, TARSKI:def 2;
A17: the InternalRel of R is_symmetric_in X by NECKLACE:def 3;
[b,a] in the InternalRel of R by A15, TARSKI:def 1;
then [a,b] in the InternalRel of R by A16, A17;
then [b,a] = [a,b] by A15, TARSKI:def 1;
hence ex a, b being object st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) by A2, XTUPLE_0:1; :: thesis: verum

end;

suppose the InternalRel of R = {[a,b],[b,a]} ; :: thesis: ex a, b being object 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 object st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) ) by A3; :: thesis: verum

end;

end;