set dx = Dependencies X;
set dox = Dependencies-Order X;
Dependencies X c= dom (Dependencies-Order X)
proof
let x be object ; :: 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 x9 = x as Element of Dependencies X ;
x9 <= x9 ;
then [x,x] in Dependencies-Order X ;
hence x in dom (Dependencies-Order X) by XTUPLE_0:def 12; :: 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 2; :: thesis: ( 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; :: thesis: ( Dependencies-Order X is antisymmetric & Dependencies-Order X is (F2) )
Dependencies-Order X is_antisymmetric_in Dependencies X
proof
let x, y be object ; :: 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 and
y in Dependencies X and
A3: [x,y] in Dependencies-Order X and
A4: [y,x] in Dependencies-Order X ; :: thesis: 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; :: thesis: verum
end;
hence Dependencies-Order X is antisymmetric by A2; :: thesis: Dependencies-Order X is (F2)
Dependencies-Order X is_transitive_in Dependencies X
proof
let x, y, z be object ; :: 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 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 ; :: thesis: [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; :: thesis: verum
end;
hence Dependencies-Order X is (F2) by A2; :: thesis: verum