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

thus T is strict ; :: thesis: T is empty

thus the carrier of T is empty ; :: according to STRUCT_0:def 1 :: thesis: verum