theorem :: WAYBEL_0:49

for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st F = uparrow x )