set R = {[{} ,{} ]};
reconsider R = {[{} ,{} ]} as Relation ;
A1: field R = {{} ,{} } by RELAT_1:32
.= {{} } by ENUMSET1:69 ;
take R ; :: thesis: ( R is reflexive & R is antisymmetric & R is (F2) & R is (C1) )
thus R is reflexive :: thesis: ( R is antisymmetric & R is (F2) & R is (C1) )

proof

let x be set ; :: 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 (F2) & R is (C1) )

proof

let x, y be set ; :: 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 ( x in field R & y in field R & [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( x = {} & y = {} ) by A1, TARSKI:def 1;
hence x = y ; :: thesis: verum

end;

thus R is (F2) :: thesis: R is (C1)

proof

let x, y, z be set ; :: 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 ( x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( x = {} & z = {} ) by A1, TARSKI:def 1;
hence [x,z] in R by TARSKI:def 1; :: thesis: verum

end;

thus R is (C1) ; :: thesis: verum