{x} c= union (MaxADSF x) by Th14;
hence not MaxADSet x is empty ; :: thesis: verum