theorem Th19: :: OPENLATT:19

for L being D_Lattice
for a, b being Element of L st not b [= a holds
<.b.) in (SF_have b) \ (SF_have a)