for L being non empty RelStr
for p being Element of L st p is completely-irreducible holds
"/\" (((uparrow p) \ {p}),L) <> p