B1: dom {} = {} ;
{} is symmetrical

proof

assume not {} is symmetrical ; :: thesis: contradiction
then consider x being complex number such that
A1: x in {} and
not - x in {} by Def1;
thus contradiction by A1; :: thesis: verum

end;

hence for b₁ being Relation st b₁ is empty holds
b₁ is with_symmetrical_domain by Def2, B1; :: thesis: verum