let S be 1-sorted ; :: thesis: ( S is empty implies S is 0 -element )
assume S is empty ; :: thesis: S is 0 -element
hence the carrier of S is 0 -element ; :: according to STRUCT_0:def 19 :: thesis: verum