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