let L be RelStr ; :: thesis: for x being set holds
( x is directed Subset of iff x is filtered Subset of )
let x be set ; :: thesis: ( x is directed Subset of iff x is filtered Subset of )
( x is filtered Subset of iff x is filtered Subset of ) by WAYBEL_0:4;
hence ( x is directed Subset of iff x is filtered Subset of ) by Th26; :: thesis: verum