let D be DB-Rel ; :: thesis: for A, B being Subset of the Attributes of D holds
( [A,B] in Dependency-str D iff A >|> B,D )
let A, B be Subset of the Attributes of D; :: thesis: ( [A,B] in Dependency-str D iff A >|> B,D )
set S = Dependency-str D;
hereby :: thesis: ( A >|> B,D implies [A,B] in Dependency-str D )
assume [A,B] in Dependency-str D ; :: thesis: A >|> B,D
then consider a, b being Subset of the Attributes of D such that
A1: [A,B] = [a,b] and
A2: a >|> b,D ;
A = a by A1, XTUPLE_0:1;
hence A >|> B,D by A1, A2, XTUPLE_0:1; :: thesis: verum
end;
thus ( A >|> B,D implies [A,B] in Dependency-str D ) ; :: thesis: verum