theorem
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)))