thus not the carrier of TopStruct(# A,t #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum