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}:]
by A1, TARSKI:def 2;
then reconsider r = {[0,1],[1,0]} as Relation of {0,1},{0,1} ;
take R = RelStr(# {0,1},r #); ( 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
for x, y being object st x in {0,1} & y in {0,1} & [x,y] in r holds
[y,x] in r
then
r is_symmetric_in {0,1}
;
hence
( not R is empty & R is strict & R is finite & R is irreflexive & R is symmetric )
by A2; verum