:: deftheorem defines ^|^ ARMSTRNG:def 17 :
for X being set
for F being Dependency-set of X
for x, y being set holds
( x ^|^ y,F iff [x,y] in Maximal_wrt F );