set dx = Dependencies X;
set dox = Dependencies-Order X;
Dependencies X c= dom (Dependencies-Order X)
then A1:
dom (Dependencies-Order X) = Dependencies X
by XBOOLE_0:def 10;
then A2: field (Dependencies-Order X) =
(Dependencies X) \/ (rng (Dependencies-Order X))
by RELAT_1:def 6
.=
Dependencies X
by XBOOLE_1:12
;
thus
Dependencies-Order X is total
by A1, PARTFUN1:def 2; ( Dependencies-Order X is reflexive & Dependencies-Order X is antisymmetric & Dependencies-Order X is (F2) )
Dependencies-Order X is_reflexive_in Dependencies X
;
hence
Dependencies-Order X is reflexive
by A2; ( Dependencies-Order X is antisymmetric & Dependencies-Order X is (F2) )
Dependencies-Order X is_antisymmetric_in Dependencies X
proof
let x,
y be
object ;
RELAT_2:def 4 ( not x in Dependencies X or not y in Dependencies X or not [x,y] in Dependencies-Order X or not [y,x] in Dependencies-Order X or x = y )
assume that
x in Dependencies X
and
y in Dependencies X
and A3:
[x,y] in Dependencies-Order X
and A4:
[y,x] in Dependencies-Order X
;
x = y
consider x9,
y9 being
Element of
Dependencies X such that A5:
[x,y] = [x9,y9]
and A6:
x9 <= y9
by A3;
A7:
y = y9
by A5, XTUPLE_0:1;
consider y99,
x99 being
Element of
Dependencies X such that A8:
[y,x] = [y99,x99]
and A9:
y99 <= x99
by A4;
A10:
x = x99
by A8, XTUPLE_0:1;
A11:
y = y99
by A8, XTUPLE_0:1;
x = x9
by A5, XTUPLE_0:1;
hence
x = y
by A6, A9, A10, A7, A11, Th11;
verum
end;
hence
Dependencies-Order X is antisymmetric
by A2; Dependencies-Order X is (F2)
Dependencies-Order X is_transitive_in Dependencies X
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( not x in Dependencies X or not y in Dependencies X or not z in Dependencies X or not [x,y] in Dependencies-Order X or not [y,z] in Dependencies-Order X or [x,z] in Dependencies-Order X )
assume that
x in Dependencies X
and
y in Dependencies X
and
z in Dependencies X
and A12:
[x,y] in Dependencies-Order X
and A13:
[y,z] in Dependencies-Order X
;
[x,z] in Dependencies-Order X
consider x9,
y9 being
Element of
Dependencies X such that A14:
[x,y] = [x9,y9]
and A15:
x9 <= y9
by A12;
A16:
x = x9
by A14, XTUPLE_0:1;
consider y99,
z9 being
Element of
Dependencies X such that A17:
[y,z] = [y99,z9]
and A18:
y99 <= z9
by A13;
A19:
y = y99
by A17, XTUPLE_0:1;
A20:
z = z9
by A17, XTUPLE_0:1;
y = y9
by A14, XTUPLE_0:1;
then
x9 <= z9
by A15, A18, A19, Th12;
hence
[x,z] in Dependencies-Order X
by A16, A20;
verum
end;
hence
Dependencies-Order X is (F2)
by A2; verum