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]}

( 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;

end;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;

end;

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;hence x in {[a,b],[b,a]} by A5, A10, NECKLACE:def 5; :: thesis: verum

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;

end;

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 = {} ) )

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

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 = {} ) )

( 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;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

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 = {} ) )

( 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;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

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 = {} ) )

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