for GX being TopStruct holds Cl ([#] GX) = [#] GX by PRE_TOPC:18;