let X be finite set ; for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
candidate-keys F = {K}
let F be Dependency-set of X; for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
candidate-keys F = {K}
let K be Subset of X; ( F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } implies candidate-keys F = {K} )
assume
F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) }
; candidate-keys F = {K}
then A1:
Maximal_wrt F = {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A }
by Th30;
hence
candidate-keys F = {K}
by TARSKI:2; verum