let R be symmetric irreflexive RelStr ; ( 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
; 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 ;
TARSKI:def 3 ( not x in the InternalRel of R or x in {[a,b],[b,a]} )
assume A5:
x in the
InternalRel of
R
;
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;
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 A12:
the
InternalRel of
R = {[a,b]}
;
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;
verum end; suppose A15:
the
InternalRel of
R = {[b,a]}
;
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;
verum end; end;