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 ;
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 ;
per cases ( x = [a,a] or x = [a,b] or x = [b,a] or x = [b,b] ) by ;
suppose A10: x = [a,a] ; :: thesis: x in {[a,b],[b,a]}
a in the carrier of R by ;
hence x in {[a,b],[b,a]} by ; :: thesis: verum
end;
suppose A11: x = [b,b] ; :: thesis: x in {[a,b],[b,a]}
b in the carrier of R by ;
hence x in {[a,b],[b,a]} by ; :: 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 ;
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 ;
A14: the InternalRel of R is_symmetric_in X by NECKLACE:def 3;
[a,b] in the InternalRel of R by ;
then [b,a] in the InternalRel of R by ;
then [b,a] = [a,b] by ;
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 ; :: 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 ;
A17: the InternalRel of R is_symmetric_in X by NECKLACE:def 3;
[b,a] in the InternalRel of R by ;
then [a,b] in the InternalRel of R by ;
then [b,a] = [a,b] by ;
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 ; :: 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;