take [#] REAL ; :: thesis: [#] REAL is symmetrical
let x be Complex; :: according to FUNCT_8:def 1 :: thesis: ( x in [#] REAL implies - x in [#] REAL )
for x being Real st x in REAL holds
- x in REAL by XREAL_0:def 1;
hence ( x in [#] REAL implies - x in [#] REAL ) ; :: thesis: verum