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 ;
let A, B, C be Subset of X; :: thesis: ( [A,B] in F & [B,C] in F implies [A,C] in F )
assume that
A2: [A,B] in F and
A3: [B,C] in F ; :: thesis: [A,C] in F
A4: B in field F by A2, RELAT_1:15;
A5: C in field F by A3, RELAT_1:15;
A in field F by A2, RELAT_1:15;
hence [A,C] in F by A1, A2, A3, A4, A5; :: thesis: verum
end;
assume A6: 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 object ; :: 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 that
A7: x in field F and
A8: y in field F and
A9: z in field F and
A10: [x,y] in F and
A11: [y,z] in F ; :: thesis: [x,z] in F
field F c= (bool X) \/ (bool X) by RELSET_1:8;
then reconsider A = x, B = y, C = z as Subset of X by A7, A8, A9;
A12: [B,C] in F by A11;
[A,B] in F by A10;
hence [x,z] in F by A6, A12; :: thesis: verum