let V, A be set ; :: thesis: 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 )
let d be TypeSCNominativeData of V,A; :: thesis: 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 )
let a, b be Element of V; :: thesis: ( ( 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 ) implies ( d in dom (less (A,b,a)) & (less (A,b,a)) . d = TRUE ) )
set e = Equality (A,a,b);
set E = Equality A;
set Da = denaming (V,A,a);
set Db = denaming (V,A,b);
set L = less A;
assume that
A1: ( ( 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 ) ) and
A2: ( a is_ext_real_on d & b is_ext_real_on d ) and
A3: d in dom (PP_not (Equality (A,a,b))) and
A4: (PP_not (Equality (A,a,b))) . d = TRUE and
A5: ( not d in dom (less (A,a,b)) or (less (A,a,b)) . d <> TRUE ) ; :: thesis: ( d in dom (less (A,b,a)) & (less (A,b,a)) . d = TRUE )
A6: a is_a_value_on d by A1;
A7: b is_a_value_on d by A1;
A8: dom <:(denaming (V,A,b)),(denaming (V,A,a)):> = (dom (denaming (V,A,b))) /\ (dom (denaming (V,A,a))) by FUNCT_3:def 7;
A9: dom (PP_not (Equality (A,a,b))) = dom (Equality (A,a,b)) by PARTPR_1:def 2;
A10: dom (Equality (A,a,b)) c= dom <:(denaming (V,A,a)),(denaming (V,A,b)):> by RELAT_1:25;
then d in dom <:(denaming (V,A,a)),(denaming (V,A,b)):> by A3, A9;
then A11: d in dom <:(denaming (V,A,b)),(denaming (V,A,a)):> by A8, FUNCT_3:def 7;
A12: (Equality (A,a,b)) . d = FALSE by A3, A4, A9, PARTPR_1:5;
A13: <:(denaming (V,A,a)),(denaming (V,A,b)):> . d = [((denaming (V,A,a)) . d),((denaming (V,A,b)) . d)] by A3, A9, A10, FUNCT_3:def 7;
then (Equality (A,a,b)) . d = (Equality A) . (((denaming (V,A,a)) . d),((denaming (V,A,b)) . d)) by A3, A9, A10, FUNCT_1:13;
then A14: (denaming (V,A,a)) . d <> (denaming (V,A,b)) . d by A6, A12, Def9;
reconsider x = (denaming (V,A,a)) . d, y = (denaming (V,A,b)) . d as ExtReal by A2;
A15: d in dom <:(denaming (V,A,a)),(denaming (V,A,b)):> by A3, A9, FUNCT_1:11;
A16: dom (less A) = [:A,A:] by FUNCT_2:def 1;
[((denaming (V,A,a)) . d),((denaming (V,A,b)) . d)] in [:A,A:] by A6, A7, ZFMISC_1:def 2;
then d in dom ((less A) * <:(denaming (V,A,a)),(denaming (V,A,b)):>) by A15, A13, A16, FUNCT_1:11;
then FALSE = ((less A) * <:(denaming (V,A,a)),(denaming (V,A,b)):>) . d by A5, PARTPR_1:3
.= (less A) . (((denaming (V,A,a)) . d),((denaming (V,A,b)) . d)) by A3, A9, A10, A13, FUNCT_1:13 ;
then not x less_pred y by A6, A7, Def12;
then A17: (denaming (V,A,b)) . d less_pred (denaming (V,A,a)) . d by A14, Th10;
((less A) * <:(denaming (V,A,b)),(denaming (V,A,a)):>) . d = (less A) . (<:(denaming (V,A,b)),(denaming (V,A,a)):> . d) by A11, FUNCT_1:13
.= (less A) . (((denaming (V,A,b)) . d),((denaming (V,A,a)) . d)) by A11, FUNCT_3:def 7
.= TRUE by A6, A7, A17, Def12 ;
hence ( d in dom (less (A,b,a)) & (less (A,b,a)) . d = TRUE ) by A1, A8, A11, Th12; :: thesis: verum