let X be set ; ( 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)
; ( 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)
( Dependencies X is (F3) & Dependencies X is (F4) )proof
let x,
y,
z be
object ;
RELAT_2:def 8,
RELAT_2:def 16 ( 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
;
[x,z] in Dependencies X
thus
[x,z] in Dependencies X
by A1, A2, A3, ZFMISC_1:def 2;
verum
end;
thus
Dependencies X is (F3)
; Dependencies X is (F4)
thus
Dependencies X is (F4)
; verum