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

[y,x] in r

hence ( not R is empty & R is strict & R is finite & R is irreflexive & R is symmetric ) by A2; :: thesis: verum

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

for x, y being object st x in {0,1} & y in {0,1} & [x,y] in r holds
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

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;A3: not [0,0] in r

proof

A4:
not [1,1] in r
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;then ( [0,0] = [0,1] or [0,0] = [1,0] ) by TARSKI:def 2;

hence contradiction by XTUPLE_0:1; :: thesis: verum

proof

assume
x in the carrier of R
; :: thesis: not [x,x] in the InternalRel of R
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;then ( [1,1] = [0,1] or [1,1] = [1,0] ) by TARSKI:def 2;

hence contradiction by XTUPLE_0:1; :: thesis: verum

then ( x = 0 or x = 1 ) by TARSKI:def 2;

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

[y,x] in r

proof

then
r is_symmetric_in {0,1}
;
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

end;assume that

x in {0,1} and

y in {0,1} and

A5: [x,y] in r ; :: thesis: [y,x] in r

hence ( not R is empty & R is strict & R is finite & R is irreflexive & R is symmetric ) by A2; :: thesis: verum