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 #); :: 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 XTUPLE_0:1; :: 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 XTUPLE_0:1; :: 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 object st x in {0,1} & y in {0,1} & [x,y] in r holds
[y,x] in r
proof
let x, y be object ; :: 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 XTUPLE_0:1;
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 XTUPLE_0:1;
hence [y,x] in r by TARSKI:def 2; :: thesis: verum
end;
end;
end;
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; :: thesis: verum