Metamath Proof Explorer


Syntax definition crtcl

Description: Extend class notation with reflexive-transitive closure.

Ref Expression
Assertion crtcl class t*