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: Dependency-str D is (DC3)

proof

let A, B be Subset of the Attributes of D; :: according to ARMSTRNG:def 16 :: thesis: ( B c= A implies [A,B] in Dependency-str D )
assume A2: 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 8 :: thesis: ( f | A = g | A implies f | B = g | B )
assume A3: f | A = g | A ; :: thesis: f | B = g | B
thus f | B = (f | A) | B by A2, RELAT_1:103
.= g | B by A2, A3, RELAT_1:103 ; :: thesis: verum

end;

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

end;

A4: now

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 ( [A,B] in Dependency-str D & [B,C] in Dependency-str D ) ; :: thesis: [A,C] in Dependency-str D
then A5: ( A >|> B,D & B >|> C,D ) by Th12;
A >|> C,D

proof

let f, g be Element of the Relationship of D; :: according to ARMSTRNG:def 8 :: 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, Def8;
hence f | C = g | C by A5, Def8; :: thesis: verum

end;

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

end;

then A6: Dependency-str D is (F2) by Th20;
hence Dependency-str D is (F1) by A1; :: according to ARMSTRNG:def 15 :: thesis: ( Dependency-str D is (F2) & Dependency-str D is (F3) & Dependency-str D is (F4) )
thus Dependency-str D is (F2) by A4, Th20; :: thesis: ( Dependency-str D is (F3) & Dependency-str D is (F4) )
thus Dependency-str D is (F3) by A1, A6; :: thesis: Dependency-str D is (F4)
thus Dependency-str D is (F4) :: thesis: verum

proof

let A, B, A', B' be Subset of the Attributes of D; :: according to ARMSTRNG:def 14 :: thesis: ( [A,B] in Dependency-str D & [A',B'] in Dependency-str D implies [(A \/ A'),(B \/ B')] in Dependency-str D )
assume ( [A,B] in Dependency-str D & [A',B'] in Dependency-str D ) ; :: thesis: [(A \/ A'),(B \/ B')] in Dependency-str D
then A7: ( A >|> B,D & A' >|> B',D ) by Th12;
A \/ A' >|> B \/ B',D

proof

let f, g be Element of the Relationship of D; :: according to ARMSTRNG:def 8 :: thesis: ( f | (A \/ A') = g | (A \/ A') implies f | (B \/ B') = g | (B \/ B') )
assume A8: f | (A \/ A') = g | (A \/ A') ; :: thesis: f | (B \/ B') = g | (B \/ B')
f | A = (f | (A \/ A')) | A by RELAT_1:103, XBOOLE_1:7
.= g | A by A8, RELAT_1:103, XBOOLE_1:7 ;
then A9: f | B = g | B by A7, Def8;
f | A' = (f | (A \/ A')) | A' by RELAT_1:103, XBOOLE_1:7
.= g | A' by A8, RELAT_1:103, XBOOLE_1:7 ;
then A10: f | B' = g | B' by A7, Def8;
thus f | (B \/ B') = (f | B) \/ (f | B') by RELAT_1:107
.= g | (B \/ B') by A9, A10, RELAT_1:107 ; :: thesis: verum

end;

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

end;