let D be DB-Rel ; :: thesis: Dependency-str D is full_family
set S = Dependency-str D;
set T = the Attributes of D;
set R = the Relationship of D;

A1: now :: thesis: for A, B, C being Subset of the Attributes of D st [A,B] in Dependency-str D & [B,C] in Dependency-str D holds
[A,C] in Dependency-str D

let A, B, C be Subset of the Attributes of D; :: thesis: ( [A,B] in Dependency-str D & [B,C] in Dependency-str D implies [A,C] in Dependency-str D )
assume that
A2: [A,B] in Dependency-str D and
A3: [B,C] in Dependency-str D ; :: thesis: [A,C] in Dependency-str D
A4: B >|> C,D by A3, Th10;
A5: A >|> B,D by A2, Th10;
A >|> C,D

proof

let f, g be Element of the Relationship of D; :: according to ARMSTRNG:def 7 :: thesis: ( f | A = g | A implies f | C = g | C )
assume f | A = g | A ; :: thesis: f | C = g | C
then f | B = g | B by A5;
hence f | C = g | C by A4; :: thesis: verum

end;

hence [A,C] in Dependency-str D ; :: thesis: verum

end;

then A6: Dependency-str D is (F2) by Th18;
A7: Dependency-str D is (DC3)

proof

let A, B be Subset of the Attributes of D; :: according to ARMSTRNG:def 15 :: thesis: ( B c= A implies [A,B] in Dependency-str D )
assume A8: B c= A ; :: thesis: [A,B] in Dependency-str D
A >|> B,D

proof

let f, g be Element of the Relationship of D; :: according to ARMSTRNG:def 7 :: thesis: ( f | A = g | A implies f | B = g | B )
assume A9: f | A = g | A ; :: thesis: f | B = g | B
thus f | B = (f | A) | B by A8, RELAT_1:74
.= g | B by A8, A9, RELAT_1:74 ; :: thesis: verum

end;

hence [A,B] in Dependency-str D ; :: thesis: verum

end;

hence Dependency-str D is (F1) ; :: according to ARMSTRNG:def 14 :: thesis: ( Dependency-str D is (F2) & Dependency-str D is (F3) & Dependency-str D is (F4) )
thus Dependency-str D is (F2) by A1, Th18; :: thesis: ( Dependency-str D is (F3) & Dependency-str D is (F4) )
thus Dependency-str D is (F3) by A7, A6; :: thesis: Dependency-str D is (F4)
thus Dependency-str D is (F4) :: thesis: verum

proof

let A, B, A9, B9 be Subset of the Attributes of D; :: according to ARMSTRNG:def 13 :: thesis: ( [A,B] in Dependency-str D & [A9,B9] in Dependency-str D implies [(A \/ A9),(B \/ B9)] in Dependency-str D )
assume that
A10: [A,B] in Dependency-str D and
A11: [A9,B9] in Dependency-str D ; :: thesis: [(A \/ A9),(B \/ B9)] in Dependency-str D
A12: A9 >|> B9,D by A11, Th10;
A13: A >|> B,D by A10, Th10;
A \/ A9 >|> B \/ B9,D

proof

let f, g be Element of the Relationship of D; :: according to ARMSTRNG:def 7 :: thesis: ( f | (A \/ A9) = g | (A \/ A9) implies f | (B \/ B9) = g | (B \/ B9) )
assume A14: f | (A \/ A9) = g | (A \/ A9) ; :: thesis: f | (B \/ B9) = g | (B \/ B9)
f | A9 = (f | (A \/ A9)) | A9 by RELAT_1:74, XBOOLE_1:7
.= g | A9 by A14, RELAT_1:74, XBOOLE_1:7 ;
then A15: f | B9 = g | B9 by A12;
f | A = (f | (A \/ A9)) | A by RELAT_1:74, XBOOLE_1:7
.= g | A by A14, RELAT_1:74, XBOOLE_1:7 ;
then A16: f | B = g | B by A13;
thus f | (B \/ B9) = (f | B) \/ (f | B9) by RELAT_1:78
.= g | (B \/ B9) by A16, A15, RELAT_1:78 ; :: thesis: verum

end;

hence [(A \/ A9),(B \/ B9)] in Dependency-str D ; :: thesis: verum

end;