let S be 2-sorted ; :: thesis: ( S is void implies S is trivial' )
assume the carrier' of S is empty ; :: according to STRUCT_0:def 13 :: thesis: S is trivial'
hence the carrier' of S is trivial ; :: according to STRUCT_0:def 21 :: thesis: verum