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;
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 11 :: thesis: [A,A] in Dependencies X
thus [A,A] in Dependencies X ; :: thesis: verum

end;

Dependencies X = nabla (bool X) by EQREL_1:def 1;
then A1: field (Dependencies X) = bool X by ORDERS_1:12;
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 that
A2: x in field (Dependencies X) and
y in field (Dependencies X) and
A3: z in field (Dependencies X) and
[x,y] in Dependencies X and
[y,z] in Dependencies X ; :: thesis: [x,z] in Dependencies X
thus [x,z] in Dependencies X by A1, A2, A3, ZFMISC_1:def 2; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;