set dox = Dependencies-Order X;
set dx = Dependencies X;
Dependencies X c= dom (Dependencies-Order X)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Dependencies X or x in dom (Dependencies-Order X) )
assume x in Dependencies X ; :: thesis: x in dom (Dependencies-Order X)
then reconsider x' = x as Element of Dependencies X ;
x' <= x' ;
then [x,x] in Dependencies-Order X ;
hence x in dom (Dependencies-Order X) by RELAT_1:def 4; :: thesis: verum

end;

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 4; :: thesis: ( Dependencies-Order X is reflexive & Dependencies-Order X is antisymmetric & Dependencies-Order X is (F2) )
Dependencies-Order X is_reflexive_in Dependencies X

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in Dependencies X or [x,x] in Dependencies-Order X )
assume x in Dependencies X ; :: thesis: [x,x] in Dependencies-Order X
then reconsider x' = x as Element of Dependencies X ;
x' <= x' ;
hence [x,x] in Dependencies-Order X ; :: thesis: verum

end;

hence Dependencies-Order X is reflexive by A2, RELAT_2:def 9; :: thesis: ( Dependencies-Order X is antisymmetric & Dependencies-Order X is (F2) )
Dependencies-Order X is_antisymmetric_in Dependencies X

proof

let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( 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 & y in Dependencies X ) and
A3: ( [x,y] in Dependencies-Order X & [y,x] in Dependencies-Order X ) ; :: thesis: x = y
consider x', y' being Element of Dependencies X such that
A4: ( [x,y] = [x',y'] & x' <= y' ) by A3;
consider y'', x'' being Element of Dependencies X such that
A5: ( [y,x] = [y'',x''] & y'' <= x'' ) by A3;
( x = x' & x = x'' & y = y' & y = y'' ) by A4, A5, ZFMISC_1:33;
hence x = y by A4, A5, Th13; :: thesis: verum

end;

hence Dependencies-Order X is antisymmetric by A2, RELAT_2:def 12; :: thesis: Dependencies-Order X is (F2)
Dependencies-Order X is_transitive_in Dependencies X

proof

let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( 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 & y in Dependencies X & z in Dependencies X ) and
A6: ( [x,y] in Dependencies-Order X & [y,z] in Dependencies-Order X ) ; :: thesis: [x,z] in Dependencies-Order X
consider x', y' being Element of Dependencies X such that
A7: ( [x,y] = [x',y'] & x' <= y' ) by A6;
consider y'', z' being Element of Dependencies X such that
A8: ( [y,z] = [y'',z'] & y'' <= z' ) by A6;
A9: ( x = x' & y = y' & y = y'' & z = z' ) by A7, A8, ZFMISC_1:33;
then x' <= z' by A7, A8, Th14;
hence [x,z] in Dependencies-Order X by A9; :: thesis: verum

end;

hence Dependencies-Order X is (F2) by A2, RELAT_2:def 16; :: thesis: verum