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:33; :: 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:33; :: 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:33;
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:33;
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 4, NECKLACE:def 6; :: thesis: verum