-theorem aaa_csx (h) (G) (L):
- â\88\80T,A. â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92[h] T.
-#h #G #L #T #A #H
-@(gcr_aaa … (csx_gcp h) (csx_gcr h) … H)
+theorem aaa_csx (G) (L):
+ â\88\80T,A. â\9d¨G,Lâ\9d© â\8a¢ T â\81\9d A â\86\92 â\9d¨G,Lâ\9d© â\8a¢ â¬\88*ð\9d\90\92 T.
+#G #L #T #A #H
+@(gcr_aaa … csx_gcp csx_gcr … H)