thus Cl ([#] GX) = [#] GX by Th27; :: according to TOPS_1:def 3 :: thesis: verum