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