let X be set ; :: thesis: ( Dependencies X is (F1) & Dependencies X is (F2) & Dependencies X is (F3) & Dependencies X is (F4) )
set D = Dependencies X;
Dependencies X = nabla (bool X) by EQREL_1:def 1;
then A1: field (Dependencies X) = bool X by ORDERS_1:97;
thus Dependencies X is (F1) :: thesis: ( Dependencies X is (F2) & Dependencies X is (F3) & Dependencies X is (F4) )

proof

let A be Subset of X; :: according to ARMSTRNG:def 12 :: thesis: [A,A] in Dependencies X
thus [A,A] in Dependencies X ; :: thesis: verum

end;

thus Dependencies X is (F2) :: thesis: ( Dependencies X is (F3) & Dependencies X is (F4) )

proof

let x, y, z be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not x in field (Dependencies X) or not y in field (Dependencies X) or not z in field (Dependencies X) or not [x,y] in Dependencies X or not [y,z] in Dependencies X or [x,z] in Dependencies X )
assume ( x in field (Dependencies X) & y in field (Dependencies X) & z in field (Dependencies X) & [x,y] in Dependencies X & [y,z] in Dependencies X ) ; :: thesis: [x,z] in Dependencies X
hence [x,z] in Dependencies X by A1, ZFMISC_1:def 2; :: thesis: verum

end;

thus Dependencies X is (F3) :: thesis: Dependencies X is (F4)

proof

let A, B, A', B' be Subset of X; :: according to ARMSTRNG:def 13 :: thesis: ( [A,B] in Dependencies X & [A,B] >= [A',B'] implies [A',B'] in Dependencies X )
thus ( [A,B] in Dependencies X & [A,B] >= [A',B'] implies [A',B'] in Dependencies X ) ; :: thesis: verum

end;

thus Dependencies X is (F4) :: thesis: verum

proof

let A, B, A', B' be Subset of X; :: according to ARMSTRNG:def 14 :: thesis: ( [A,B] in Dependencies X & [A',B'] in Dependencies X implies [(A \/ A'),(B \/ B')] in Dependencies X )
thus ( [A,B] in Dependencies X & [A',B'] in Dependencies X implies [(A \/ A'),(B \/ B')] in Dependencies X ) ; :: thesis: verum

end;