let V, A be set ; :: 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 ) & ( 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)))
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 ) & ( 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 ) implies PP_not (Equality (A,a,b)) = PP_or ((less (A,a,b)),(less (A,b,a))) )
set e = Equality (A,a,b);
set p = PP_not (Equality (A,a,b));
set q = less (A,a,b);
set r = less (A,b,a);
set o = PP_or ((less (A,a,b)),(less (A,b,a)));
set L = less A;
set E = Equality A;
set Da = denaming (V,A,a);
set Db = denaming (V,A,b);
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: ( ( 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 ) ) ; :: thesis: PP_not (Equality (A,a,b)) = PP_or ((less (A,a,b)),(less (A,b,a)))
A3: dom (PP_not (Equality (A,a,b))) = dom (Equality (A,a,b)) by PARTPR_1:def 2;
A4: dom (PP_or ((less (A,a,b)),(less (A,b,a)))) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom (less (A,a,b)) & (less (A,a,b)) . d = TRUE ) or ( d in dom (less (A,b,a)) & (less (A,b,a)) . d = TRUE ) or ( d in dom (less (A,a,b)) & (less (A,a,b)) . d = FALSE & d in dom (less (A,b,a)) & (less (A,b,a)) . d = FALSE ) ) } by NOMIN_2:16;
A5: dom (denaming (V,A,a)) = { d where d is NonatomicND of V,A : a in dom d } by NOMIN_1:def 18;
A6: dom <:(denaming (V,A,a)),(denaming (V,A,b)):> = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by FUNCT_3:def 7;
A7: dom <:(denaming (V,A,b)),(denaming (V,A,a)):> = (dom (denaming (V,A,b))) /\ (dom (denaming (V,A,a))) by FUNCT_3:def 7;
A8: dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by A1, Th11;
A9: dom (less (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by A1, Th12;
A10: dom (less (A,b,a)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by A1, Th12;
thus dom (PP_not (Equality (A,a,b))) = dom (PP_or ((less (A,a,b)),(less (A,b,a)))) :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (PP_not (Equality (A,a,b))) or (PP_not (Equality (A,a,b))) . b1 = (PP_or ((less (A,a,b)),(less (A,b,a)))) . b1 )
proof
thus dom (PP_not (Equality (A,a,b))) c= dom (PP_or ((less (A,a,b)),(less (A,b,a)))) :: according to XBOOLE_0:def 10 :: thesis: dom (PP_or ((less (A,a,b)),(less (A,b,a)))) c= dom (PP_not (Equality (A,a,b)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_not (Equality (A,a,b))) or x in dom (PP_or ((less (A,a,b)),(less (A,b,a)))) )
assume A11: x in dom (PP_not (Equality (A,a,b))) ; :: thesis: x in dom (PP_or ((less (A,a,b)),(less (A,b,a))))
then x in dom (denaming (V,A,a)) by A3, A8, XBOOLE_0:def 4;
then ex da being NonatomicND of V,A st
( x = da & a in dom da ) by A5;
then reconsider x = x as TypeSCNominativeData of V,A ;
A12: <:(denaming (V,A,a)),(denaming (V,A,b)):> . x = [((denaming (V,A,a)) . x),((denaming (V,A,b)) . x)] by A3, A6, A8, A11, FUNCT_3:def 7;
A13: <:(denaming (V,A,b)),(denaming (V,A,a)):> . x = [((denaming (V,A,b)) . x),((denaming (V,A,a)) . x)] by A3, A7, A8, A11, FUNCT_3:def 7;
A14: ( a is_a_value_on x & b is_a_value_on x ) by A1;
A15: (less (A,a,b)) . x = (less A) . (((denaming (V,A,a)) . x),((denaming (V,A,b)) . x)) by A3, A6, A8, A11, A12, FUNCT_1:13;
A16: (less (A,b,a)) . x = (less A) . (((denaming (V,A,b)) . x),((denaming (V,A,a)) . x)) by A3, A7, A8, A11, A13, FUNCT_1:13;
A17: ( a is_ext_real_on x & b is_ext_real_on x ) by A2;
per cases ( (denaming (V,A,a)) . x = (denaming (V,A,b)) . x or (denaming (V,A,a)) . x <> (denaming (V,A,b)) . x ) ;
suppose (denaming (V,A,a)) . x = (denaming (V,A,b)) . x ; :: thesis: x in dom (PP_or ((less (A,a,b)),(less (A,b,a))))
then ( (less (A,a,b)) . x = FALSE & (less (A,b,a)) . x = FALSE ) by A14, A15, A16, Def12;
hence x in dom (PP_or ((less (A,a,b)),(less (A,b,a)))) by A3, A4, A8, A9, A10, A11; :: thesis: verum
end;
suppose A18: (denaming (V,A,a)) . x <> (denaming (V,A,b)) . x ; :: thesis: x in dom (PP_or ((less (A,a,b)),(less (A,b,a))))
now :: thesis: ( (less (A,a,b)) . x <> TRUE implies not (less (A,b,a)) . x <> TRUE )
assume ( (less (A,a,b)) . x <> TRUE & (less (A,b,a)) . x <> TRUE ) ; :: thesis: contradiction
then ( not (denaming (V,A,a)) . x less_pred (denaming (V,A,b)) . x & not (denaming (V,A,b)) . x less_pred (denaming (V,A,a)) . x ) by A14, A15, A16, Def12;
hence contradiction by A17, A18, Th10; :: thesis: verum
end;
hence x in dom (PP_or ((less (A,a,b)),(less (A,b,a)))) by A3, A4, A8, A9, A10, A11; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_or ((less (A,a,b)),(less (A,b,a)))) or x in dom (PP_not (Equality (A,a,b))) )
assume x in dom (PP_or ((less (A,a,b)),(less (A,b,a)))) ; :: thesis: x in dom (PP_not (Equality (A,a,b)))
then ex d being TypeSCNominativeData of V,A st
( x = d & ( ( d in dom (less (A,a,b)) & (less (A,a,b)) . d = TRUE ) or ( d in dom (less (A,b,a)) & (less (A,b,a)) . d = TRUE ) or ( d in dom (less (A,a,b)) & (less (A,a,b)) . d = FALSE & d in dom (less (A,b,a)) & (less (A,b,a)) . d = FALSE ) ) ) by A4;
hence x in dom (PP_not (Equality (A,a,b))) by A1, A3, A8, Th12; :: thesis: verum
end;
let x be object ; :: thesis: ( not x in dom (PP_not (Equality (A,a,b))) or (PP_not (Equality (A,a,b))) . x = (PP_or ((less (A,a,b)),(less (A,b,a)))) . x )
assume A19: x in dom (PP_not (Equality (A,a,b))) ; :: thesis: (PP_not (Equality (A,a,b))) . x = (PP_or ((less (A,a,b)),(less (A,b,a)))) . x
then x in dom (denaming (V,A,a)) by A3, A8, XBOOLE_0:def 4;
then consider da being NonatomicND of V,A such that
A20: x = da and
a in dom da by A5;
reconsider x = x as TypeSCNominativeData of V,A by A20;
A21: ( x in dom (less (A,a,b)) & x in dom (less (A,b,a)) ) by A1, A3, A8, A19, Th12;
A22: <:(denaming (V,A,a)),(denaming (V,A,b)):> . x = [((denaming (V,A,a)) . x),((denaming (V,A,b)) . x)] by A3, A6, A8, A19, FUNCT_3:def 7;
A23: <:(denaming (V,A,b)),(denaming (V,A,a)):> . x = [((denaming (V,A,b)) . x),((denaming (V,A,a)) . x)] by A3, A7, A8, A19, FUNCT_3:def 7;
A24: ( a is_a_value_on x & b is_a_value_on x ) by A1;
A25: (less (A,a,b)) . x = (less A) . (((denaming (V,A,a)) . x),((denaming (V,A,b)) . x)) by A3, A6, A8, A19, A22, FUNCT_1:13;
A26: (less (A,b,a)) . x = (less A) . (((denaming (V,A,b)) . x),((denaming (V,A,a)) . x)) by A3, A7, A8, A19, A23, FUNCT_1:13;
A27: ( a is_ext_real_on x & b is_ext_real_on x ) by A2;
per cases ( (denaming (V,A,a)) . x = (denaming (V,A,b)) . x or (denaming (V,A,a)) . x <> (denaming (V,A,b)) . x ) ;
suppose A28: (denaming (V,A,a)) . x = (denaming (V,A,b)) . x ; :: thesis: (PP_not (Equality (A,a,b))) . x = (PP_or ((less (A,a,b)),(less (A,b,a)))) . x
then ( (less (A,a,b)) . x = FALSE & (less (A,b,a)) . x = FALSE ) by A24, A25, A26, Def12;
then A29: (PP_or ((less (A,a,b)),(less (A,b,a)))) . x = FALSE by A21, PARTPR_1:def 4;
(Equality (A,a,b)) . x = (Equality A) . (((denaming (V,A,a)) . x),((denaming (V,A,b)) . x)) by A3, A19, A22, FUNCT_1:12
.= TRUE by A24, A28, Def9 ;
hence (PP_not (Equality (A,a,b))) . x = (PP_or ((less (A,a,b)),(less (A,b,a)))) . x by A29, A3, A19, PARTPR_1:def 2; :: thesis: verum
end;
suppose A30: (denaming (V,A,a)) . x <> (denaming (V,A,b)) . x ; :: thesis: (PP_not (Equality (A,a,b))) . x = (PP_or ((less (A,a,b)),(less (A,b,a)))) . x
now :: thesis: ( (less (A,a,b)) . x <> TRUE implies not (less (A,b,a)) . x <> TRUE )
assume ( (less (A,a,b)) . x <> TRUE & (less (A,b,a)) . x <> TRUE ) ; :: thesis: contradiction
then ( not (denaming (V,A,a)) . x less_pred (denaming (V,A,b)) . x & not (denaming (V,A,b)) . x less_pred (denaming (V,A,a)) . x ) by A24, A25, A26, Def12;
hence contradiction by A27, A30, Th10; :: thesis: verum
end;
then A31: (PP_or ((less (A,a,b)),(less (A,b,a)))) . x = TRUE by A21, PARTPR_1:def 4;
(Equality (A,a,b)) . x = (Equality A) . (((denaming (V,A,a)) . x),((denaming (V,A,b)) . x)) by A3, A19, A22, FUNCT_1:12
.= FALSE by A24, A30, Def9 ;
hence (PP_not (Equality (A,a,b))) . x = (PP_or ((less (A,a,b)),(less (A,b,a)))) . x by A31, A3, A19, PARTPR_1:def 2; :: thesis: verum
end;
end;