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

let A, B, C be Subset of ; :: 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, Th12;
A5: A >|> B,D by A2, 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 A4, Def8; :: thesis: verum

end;

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

end;

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

proof

let A, B be Subset of ; :: according to ARMSTRNG:def 16 :: 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 8 :: 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:103
.= g | B by A8, A9, RELAT_1:103 ; :: thesis: verum

end;

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

end;

hence Dependency-str D is (F1) by A6; :: 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 A1, Th20; :: 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, A', B' be Subset of ; :: 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 that
A10: [A,B] in Dependency-str D and
A11: [A',B'] in Dependency-str D ; :: thesis: [(A \/ A'),(B \/ B')] in Dependency-str D
A12: A' >|> B',D by A11, Th12;
A13: A >|> B,D by A10, 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 A14: 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 A14, RELAT_1:103, XBOOLE_1:7 ;
then A15: f | B' = g | B' by A12, Def8;
f | A = (f | (A \/ A')) | A by RELAT_1:103, XBOOLE_1:7
.= g | A by A14, RELAT_1:103, XBOOLE_1:7 ;
then A16: f | B = g | B by A13, Def8;
thus f | (B \/ B') = (f | B) \/ (f | B') by RELAT_1:107
.= g | (B \/ B') by A16, A15, RELAT_1:107 ; :: thesis: verum

end;

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

end;