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 )
A1: for x being Real st x in REAL holds
- x in REAL ;
thus ( x in [#] REAL implies - x in [#] REAL ) by A1; :: thesis: verum