the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence not the carrier of (MaxADSspace A) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum