take [#] REAL ; :: thesis: [#] REAL is symmetrical
let x be complex number ; :: 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 ;
hence ( x in [#] REAL implies - x in [#] REAL ) ; :: thesis: verum