let X be set ; :: thesis: for F being Dependency-set of X holds
( F is (F1) & F is (F2) & F is (F3) & F is (F4) iff ( F is (DC2) & F is (DC5) & F is (DC6) ) )
let F be Dependency-set of X; :: thesis: ( F is (F1) & F is (F2) & F is (F3) & F is (F4) iff ( F is (DC2) & F is (DC5) & F is (DC6) ) )
hereby :: thesis: ( F is (DC2) & F is (DC5) & F is (DC6) implies ( F is (F1) & F is (F2) & F is (F3) & F is (F4) ) )
assume that
A1: F is (F1) and
A2: F is (F2) and
A3: F is (F3) and
A4: F is (F4) ; :: thesis: ( F is (DC2) & F is (DC5) & F is (DC6) )
thus F is (DC2) by A1; :: thesis: ( F is (DC5) & F is (DC6) )
thus F is (DC5) :: thesis: F is (DC6)
proof
let A, B, C, D be Subset of X; :: according to ARMSTRNG:def 29 :: thesis: ( [A,B] in F & [(B \/ C),D] in F implies [(A \/ C),D] in F )
assume that
A5: [A,B] in F and
A6: [(B \/ C),D] in F ; :: thesis: [(A \/ C),D] in F
[C,C] in F by A1;
then [(A \/ C),(B \/ C)] in F by A4, A5;
hence [(A \/ C),D] in F by A2, A6, Th18; :: thesis: verum
end;
thus F is (DC6) :: thesis: verum
proof
let A, B, C be Subset of X; :: according to ARMSTRNG:def 30 :: thesis: ( [A,B] in F implies [(A \/ C),B] in F )
assume A7: [A,B] in F ; :: thesis: [(A \/ C),B] in F
A c= A \/ C by XBOOLE_1:7;
then [(A \/ C),A] in F by A1, A3, Def15;
hence [(A \/ C),B] in F by A2, A7, Th18; :: thesis: verum
end;
end;
assume that
A8: F is (DC2) and
A9: F is (DC5) and
A10: F is (DC6) ; :: thesis: ( F is (F1) & F is (F2) & F is (F3) & F is (F4) )
thus F is (F1) by A8; :: thesis: ( F is (F2) & F is (F3) & F is (F4) )
A11: now :: thesis: for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in 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
A12: [A,B] in F and
A13: [B,C] in F ; :: thesis: [A,C] in F
[(B \/ A),C] in F by A10, A13;
then [(A \/ A),C] in F by A9, A12;
hence [A,C] in F ; :: thesis: verum
end;
hence F is (F2) by Th18; :: thesis: ( F is (F3) & F is (F4) )
thus F is (F3) :: thesis: F is (F4)
proof
let A, B, A9, B9 be Subset of X; :: according to ARMSTRNG:def 12 :: thesis: ( [A,B] in F & [A,B] >= [A9,B9] implies [A9,B9] in F )
assume that
A14: [A,B] in F and
A15: [A,B] >= [A9,B9] ; :: thesis: [A9,B9] in F
A c= A9 by A15;
then A9 = A \/ (A9 \ A) by XBOOLE_1:45;
then A16: [A9,B] in F by A10, A14;
B9 c= B by A15;
then A17: B = B9 \/ (B \ B9) by XBOOLE_1:45;
[B9,B9] in F by A8;
then [B,B9] in F by A10, A17;
hence [A9,B9] in F by A11, A16; :: thesis: verum
end;
let A, B, A9, B9 be Subset of X; :: according to ARMSTRNG:def 13 :: thesis: ( [A,B] in F & [A9,B9] in F implies [(A \/ A9),(B \/ B9)] in F )
assume that
A18: [A,B] in F and
A19: [A9,B9] in F ; :: thesis: [(A \/ A9),(B \/ B9)] in F
[(B \/ B9),(B \/ B9)] in F by A8;
then [(A \/ B9),(B \/ B9)] in F by A9, A18;
hence [(A \/ A9),(B \/ B9)] in F by A9, A19; :: thesis: verum