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

A2: the carrier of S c= the carrier of L by YELLOW_0:def 13;
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 that
A3: x in X and
A4: y in X ; :: thesis: ex b₁ being Element of the carrier of S st
( b₁ in X & x <= b₁ & y <= b₁ )
A5: y in the carrier of S by A3;
x in the carrier of S by A3;
then reconsider x9 = x, y9 = y as Element of L by A5, A2;
consider z being Element of L such that
A6: z in X and
A7: z >= x9 and
A8: z >= y9 by A1, A3, A4, WAYBEL_0:def 1;
reconsider z = z as Element of S by A6;
take z ; :: thesis: ( z in X & x <= z & y <= z )
thus ( z in X & x <= z & y <= z ) by A6, A7, A8, YELLOW_0:60; :: thesis: verum

end;

end;

assume A9: X is filtered Subset of L ; :: thesis: X is filtered
A10: the carrier of S c= the carrier of L by YELLOW_0:def 13;
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 that
A11: x in X and
A12: y in X ; :: thesis: ex b₁ being Element of the carrier of S st
( b₁ in X & b₁ <= x & b₁ <= y )
A13: y in the carrier of S by A11;
x in the carrier of S by A11;
then reconsider x9 = x, y9 = y as Element of L by A13, A10;
consider z being Element of L such that
A14: z in X and
A15: z <= x9 and
A16: z <= y9 by A9, A11, A12, WAYBEL_0:def 2;
reconsider z = z as Element of S by A14;
take z ; :: thesis: ( z in X & z <= x & z <= y )
thus ( z in X & z <= x & z <= y ) by A14, A15, A16, YELLOW_0:60; :: thesis: verum