set R = {[{},{}]};
reconsider R = {[{},{}]} as Relation ;
take R ; :: thesis: ( R is reflexive & R is antisymmetric & R is transitive & not R is empty )
A1: field R = {{},{}} by RELAT_1:17
.= {{}} by ENUMSET1:29 ;
thus R is reflexive :: thesis: ( R is antisymmetric & R is transitive & not R is empty )
proof
let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not x in field R or [x,x] in R )
assume x in field R ; :: thesis: [x,x] in R
then x = {} by A1, TARSKI:def 1;
hence [x,x] in R by TARSKI:def 1; :: thesis: verum
end;
thus R is antisymmetric :: thesis: ( R is transitive & not R is empty )
proof
let x, y be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y )
assume that
A2: x in field R and
A3: y in field R and
[x,y] in R and
[y,x] in R ; :: thesis: x = y
x = {} by A1, A2, TARSKI:def 1;
hence x = y by A1, A3, TARSKI:def 1; :: thesis: verum
end;
thus R is transitive :: thesis: not R is empty
proof
let x, y, z be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A4: x in field R and
y in field R and
A5: z in field R and
[x,y] in R and
[y,z] in R ; :: thesis: [x,z] in R
A6: z = {} by A1, A5, TARSKI:def 1;
x = {} by A1, A4, TARSKI:def 1;
hence [x,z] in R by A6, TARSKI:def 1; :: thesis: verum
end;
thus not R is empty ; :: thesis: verum