theorem Th28: :: WAYBEL16:28

for L being distributive LATTICE
for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
not u "/\" q <= p