let V be RealLinearSpace; :: thesis: Cir ({} V) = {}
{} V in Circled-Family ({} V) by Def2;
hence Cir ({} V) = {} by SETFAM_1:4; :: thesis: verum