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