Liveness and safety property in formal verification

I am unable to understand the text provided in the attched pic. Can anyone please explain it. Also what is #=#?

You appear to be looking at documentation for a particular tool. This Siemens sponsored public forum is not for discussing tool specific issues. Please read your tool’s User Manual or contact your tool vendor for support.

The #=# operator is defined in the IEEE 1800-2023 SystemVerilog LRM. You may also want to read: Why can't we use followed by instead of implication operator in SVA as the default operator? - #3 by user49