take T = 1-sorted(# {} #); :: thesis: ( T is strict & T is empty )
thus T is strict ; :: thesis: T is empty
thus the carrier of T is empty ; :: according to STRUCT_0:def 1 :: thesis: verum