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 )

hereby :: thesis: ( x is filtered Subset of implies x is directed Subset of )

assume x is directed Subset of ; :: thesis: x is filtered Subset of
then reconsider X = x as directed Subset of ;
reconsider Y = X as Subset of ;
Y is filtered

proof

let x, y be Element of ; :: according to WAYBEL_0:def 2 :: thesis: ( not x in Y or not y in Y or ex b₁ being Element of the carrier of (L opp ) st
( b₁ in Y & b₁ <= x & b₁ <= y ) )
assume ( x in Y & y in Y ) ; :: thesis: ex b₁ being Element of the carrier of (L opp ) st
( b₁ in Y & b₁ <= x & b₁ <= y )
then consider z being Element of such that
A1: ( z in X & z >= ~ x & z >= ~ y ) by WAYBEL_0:def 1;
take z ~ ; :: thesis: ( z ~ in Y & z ~ <= x & z ~ <= y )
~ (z ~ ) = z ~ ;
hence ( z ~ in Y & z ~ <= x & z ~ <= y ) by A1, Th1; :: thesis: verum

end;

hence x is filtered Subset of ; :: thesis: verum

end;

assume x is filtered Subset of ; :: thesis: x is directed Subset of
then reconsider X = x as filtered Subset of ;
reconsider Y = X as Subset of ;
Y is directed

proof

let x, y be Element of ; :: according to WAYBEL_0:def 1 :: thesis: ( not x in Y or not y in Y or ex b₁ being Element of the carrier of L st
( b₁ in Y & x <= b₁ & y <= b₁ ) )
assume ( x in Y & y in Y ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in Y & x <= b₁ & y <= b₁ )
then consider z being Element of such that
A2: ( z in X & z <= x ~ & z <= y ~ ) by WAYBEL_0:def 2;
take ~ z ; :: thesis: ( ~ z in Y & x <= ~ z & y <= ~ z )
(~ z) ~ = ~ z ;
hence ( ~ z in Y & x <= ~ z & y <= ~ z ) by A2, LATTICE3:9; :: thesis: verum

end;

hence x is directed Subset of ; :: thesis: verum