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 )
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 A2: ( x in {0 ,1} & y in {0 ,1} & [x,y] in r ) ; :: thesis: [y,x] in r

per cases ( [x,y] = [0 ,1] or [x,y] = [1,0 ] ) by A2, 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 A3: r is_symmetric_in {0 ,1} by RELAT_2:def 3;
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 )
assume x in the carrier of R ; :: thesis: not [x,x] in the InternalRel of R
then A4: ( x = 0 or x = 1 ) by TARSKI:def 2;
A5: 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;

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;

hence not [x,x] in the InternalRel of R by A4, A5; :: thesis: verum

end;

hence ( not R is empty & R is strict & R is finite & R is irreflexive & R is symmetric ) by A3, NECKLACE:def 4, NECKLACE:def 6; :: thesis: verum