theorem :: NOMIN_4:13

for V, A being set
for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds a is_ext_real_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_ext_real_on d ) holds
PP_not (Equality (A,a,b)) = PP_or ((less (A,a,b)),(less (A,b,a)))