take S = 2-sorted(# {},{} #); :: thesis: ( S is strict & S is empty & S is void )
thus S is strict ; :: thesis: ( S is empty & S is void )
thus the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: S is void
thus the carrier' of S is empty ; :: according to STRUCT_0:def 13 :: thesis: verum