:: deftheorem defines principal WAYBEL_0:def 22 :
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
( x in F & x is_<=_than F ) );