let X be set ; :: thesis: for F being Dependency-set of X holds
( F is (F2) iff for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F )
let F be Dependency-set of X; :: thesis: ( F is (F2) iff for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F )

hereby :: thesis: ( ( for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F ) implies F is (F2) )

assume F is (F2) ; :: thesis: for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F
then A1: F is_transitive_in field F by RELAT_2:def 16;
let A, B, C be Subset of X; :: thesis: ( [A,B] in F & [B,C] in F implies [A,C] in F )
assume A2: ( [A,B] in F & [B,C] in F ) ; :: thesis: [A,C] in F
then ( A in field F & B in field F & C in field F ) by RELAT_1:30;
hence [A,C] in F by A1, A2, RELAT_2:def 8; :: thesis: verum

end;

assume A3: for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F ; :: thesis: F is (F2)
let x, y, z be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not x in field F or not y in field F or not z in field F or not [x,y] in F or not [y,z] in F or [x,z] in F )
assume A4: ( x in field F & y in field F & z in field F & [x,y] in F & [y,z] in F ) ; :: thesis: [x,z] in F
field F c= (bool X) \/ (bool X) by RELSET_1:19;
then reconsider A = x, B = y, C = z as Subset of X by A4;
( [A,B] in F & [B,C] in F ) by A4;
hence [x,z] in F by A3; :: thesis: verum