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

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

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

thus not S is void ; :: thesis: ( S is trivial & S is trivial' )

thus S is trivial ; :: thesis: S is trivial'

thus the carrier' of S is trivial ; :: according to STRUCT_0:def 21 :: thesis: verum

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

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

thus not S is void ; :: thesis: ( S is trivial & S is trivial' )

thus S is trivial ; :: thesis: S is trivial'

thus the carrier' of S is trivial ; :: according to STRUCT_0:def 21 :: thesis: verum