let A1, A2 be AdjectiveStr ; :: thesis: ( the adjectives of A1 = the adjectives of A2 & A1 is void implies A2 is void )
assume A1: the adjectives of A1 = the adjectives of A2 ; :: thesis: ( not A1 is void or A2 is void )
assume the adjectives of A1 is empty ; :: according to ABCMIZ_0:def 4 :: thesis: A2 is void
hence the adjectives of A2 is empty by A1; :: according to ABCMIZ_0:def 4 :: thesis: verum