for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is directed