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