theorem :: NOMIN_4:14

for V, A being set
for d being TypeSCNominativeData of V,A
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 ) & a is_ext_real_on d & b is_ext_real_on d & d in dom (PP_not (Equality (A,a,b))) & (PP_not (Equality (A,a,b))) . d = TRUE & not ( d in dom (less (A,a,b)) & (less (A,a,b)) . d = TRUE ) holds
( d in dom (less (A,b,a)) & (less (A,b,a)) . d = TRUE )