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) )
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 object ; :: 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)
thus Dependencies X is (F4) ; :: thesis: verum