take S = 2-sorted(# {0},{0} #); :: thesis: ( S is strict & not S is empty & not S is void )

thus S is strict ; :: thesis: ( not S is empty & not S is void )

thus not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: not S is void

thus not the carrier' of S is empty ; :: according to STRUCT_0:def 13 :: thesis: verum

thus S is strict ; :: thesis: ( not S is empty & not S is void )

thus not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: not S is void

thus not the carrier' of S is empty ; :: according to STRUCT_0:def 13 :: thesis: verum