let L be RelStr ; :: thesis: for S being full SubRelStr of L
for X being Subset of S holds
( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )
let S be full SubRelStr of L; :: thesis: for X being Subset of S holds
( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )
let X be Subset of S; :: thesis: ( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )

hereby :: thesis: ( X is filtered Subset of L implies X is filtered )

assume A1: X is directed Subset of L ; :: thesis: X is directed
thus X is directed :: thesis: verum

proof

let x, y be Element of S; :: according to WAYBEL_0:def 1 :: thesis: ( not x in X or not y in X or ex b₁ being Element of the carrier of S st
( b₁ in X & x <= b₁ & y <= b₁ ) )
assume A2: ( x in X & y in X ) ; :: thesis: ex b₁ being Element of the carrier of S st
( b₁ in X & x <= b₁ & y <= b₁ )
then ( x in the carrier of S & y in the carrier of S & the carrier of S c= the carrier of L ) by YELLOW_0:def 13;
then reconsider x' = x, y' = y as Element of L ;
consider z being Element of L such that
A3: ( z in X & z >= x' & z >= y' ) by A1, A2, WAYBEL_0:def 1;
reconsider z = z as Element of S by A3;
take z ; :: thesis: ( z in X & x <= z & y <= z )
thus ( z in X & x <= z & y <= z ) by A3, YELLOW_0:61; :: thesis: verum

end;

end;

assume A4: X is filtered Subset of L ; :: thesis: X is filtered
let x, y be Element of S; :: according to WAYBEL_0:def 2 :: thesis: ( not x in X or not y in X or ex b₁ being Element of the carrier of S st
( b₁ in X & b₁ <= x & b₁ <= y ) )
assume A5: ( x in X & y in X ) ; :: thesis: ex b₁ being Element of the carrier of S st
( b₁ in X & b₁ <= x & b₁ <= y )
then ( x in the carrier of S & y in the carrier of S & the carrier of S c= the carrier of L ) by YELLOW_0:def 13;
then reconsider x' = x, y' = y as Element of L ;
consider z being Element of L such that
A6: ( z in X & z <= x' & z <= y' ) by A4, A5, WAYBEL_0:def 2;
reconsider z = z as Element of S by A6;
take z ; :: thesis: ( z in X & z <= x & z <= y )
thus ( z in X & z <= x & z <= y ) by A6, YELLOW_0:61; :: thesis: verum