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 (DC1) & F is (DC3) & F is (DC4) ) )
let F be Dependency-set of X; :: thesis: ( F is (F1) & F is (F2) & F is (F3) & F is (F4) iff ( F is (DC1) & F is (DC3) & F is (DC4) ) )
hereby :: thesis: ( F is (DC1) & F is (DC3) & F is (DC4) 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 (DC1) & F is (DC3) & F is (DC4) )
thus F is (DC1) by A2; :: thesis: ( F is (DC3) & F is (DC4) )
thus F is (DC3) by A1, A3; :: thesis: F is (DC4)
thus F is (DC4) :: thesis: verum
proof
let A, B, C be Subset of X; :: according to ARMSTRNG:def 28 :: thesis: ( [A,B] in F & [A,C] in F implies [A,(B \/ C)] in F )
assume that
A5: [A,B] in F and
A6: [A,C] in F ; :: thesis: [A,(B \/ C)] in F
[(A \/ A),(B \/ C)] in F by A4, A5, A6;
hence [A,(B \/ C)] in F ; :: thesis: verum
end;
end;
assume that
A7: F is (DC1) and
A8: F is (DC3) and
A9: F is (DC4) ; :: 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) )
thus F is (F2) by A7; :: thesis: ( F is (F3) & F is (F4) )
thus F is (F3) by A7, A8; :: thesis: F is (F4)
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
A10: [A,B] in F and
A11: [A9,B9] in F ; :: thesis: [(A \/ A9),(B \/ B9)] in F
A9 c= A \/ A9 by XBOOLE_1:7;
then [(A \/ A9),A9] in F by A8;
then A12: [(A \/ A9),B9] in F by A7, A11, Th18;
A c= A \/ A9 by XBOOLE_1:7;
then [(A \/ A9),A] in F by A8;
then [(A \/ A9),B] in F by A7, A10, Th18;
hence [(A \/ A9),(B \/ B9)] in F by A9, A12; :: thesis: verum