:: HERMITAN semantic presentation
begin
theorem
:: HERMITAN:1
for
a
being (
number
) holds