let L be RelStr ; :: thesis: for x being set holds
( x is directed Subset of L iff x is filtered Subset of (L opp) )
let x be set ; :: thesis: ( x is directed Subset of L iff x is filtered Subset of (L opp) )

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

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

proof

let x, y be Element of (L opp); :: 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 L 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 (L opp) ; :: thesis: verum

end;

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

proof

let x, y be Element of L; :: 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 (L opp) 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 L ; :: thesis: verum