set X = {0,1};
set r = {[0,1],[1,0]};
( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def 2;
then A1: ( [0,1] in [:{0,1},{0,1}:] & [1,0] in [:{0,1},{0,1}:] ) by ZFMISC_1:def 2;
{[0,1],[1,0]} c= [:{0,1},{0,1}:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[0,1],[1,0]} or x in [:{0,1},{0,1}:] )
assume x in {[0,1],[1,0]} ; :: thesis: x in [:{0,1},{0,1}:]
hence x in [:{0,1},{0,1}:] by A1, TARSKI:def 2; :: thesis: verum

end;

then reconsider r = {[0,1],[1,0]} as Relation of {0,1},{0,1} ;
take R = RelStr(# {0,1},r #); :: thesis: ( not R is empty & R is strict & R is finite & R is irreflexive & R is symmetric )
A2: for x being set st x in the carrier of R holds
not [x,x] in the InternalRel of R

proof

let x be set ; :: thesis: ( x in the carrier of R implies not [x,x] in the InternalRel of R )
A3: not [0,0] in r

proof

assume [0,0] in r ; :: thesis: contradiction
then ( [0,0] = [0,1] or [0,0] = [1,0] ) by TARSKI:def 2;
hence contradiction by ZFMISC_1:27; :: thesis: verum

end;

A4: not [1,1] in r

proof

assume [1,1] in r ; :: thesis: contradiction
then ( [1,1] = [0,1] or [1,1] = [1,0] ) by TARSKI:def 2;
hence contradiction by ZFMISC_1:27; :: thesis: verum

end;

assume x in the carrier of R ; :: thesis: not [x,x] in the InternalRel of R
then ( x = 0 or x = 1 ) by TARSKI:def 2;
hence not [x,x] in the InternalRel of R by A3, A4; :: thesis: verum

end;

for x, y being set st x in {0,1} & y in {0,1} & [x,y] in r holds
[y,x] in r

proof

let x, y be set ; :: thesis: ( x in {0,1} & y in {0,1} & [x,y] in r implies [y,x] in r )
assume that
x in {0,1} and
y in {0,1} and
A5: [x,y] in r ; :: thesis: [y,x] in r

per cases ( [x,y] = [0,1] or [x,y] = [1,0] ) by A5, TARSKI:def 2;

suppose [x,y] = [0,1] ; :: thesis: [y,x] in r

then ( x = 0 & y = 1 ) by ZFMISC_1:27;
hence [y,x] in r by TARSKI:def 2; :: thesis: verum

end;

suppose [x,y] = [1,0] ; :: thesis: [y,x] in r

then ( x = 1 & y = 0 ) by ZFMISC_1:27;
hence [y,x] in r by TARSKI:def 2; :: thesis: verum

end;

end;

end;

then r is_symmetric_in {0,1} by RELAT_2:def 3;
hence ( not R is empty & R is strict & R is finite & R is irreflexive & R is symmetric ) by A2, NECKLACE:def 3, NECKLACE:def 5; :: thesis: verum