take X = 1-sorted(# the C -element set #); :: thesis: X is C -element
thus the carrier of X is C -element ; :: according to STRUCT_0:def 19 :: thesis: verum