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