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

proof

assume A1: X is directed Subset of S ; :: thesis: X is directed Subset of L
the carrier of S c= the carrier of L by YELLOW_0:def 13;
then reconsider X = X as Subset of L by A1, XBOOLE_1:1;
for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z )

proof

let x, y be Element of L; :: thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume A2: ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
then reconsider x' = x, y' = y as Element of S by A1;
consider z being Element of S such that
A3: z in X and
A4: ( x' <= z & y' <= z ) by A1, A2, WAYBEL_0:def 1;
reconsider z = z as Element of L by YELLOW_0:59;
take z ; :: thesis: ( z in X & x <= z & y <= z )
thus ( z in X & x <= z & y <= z ) by A3, A4, YELLOW_0:60; :: thesis: verum

end;

hence X is directed Subset of L by WAYBEL_0:def 1; :: thesis: verum

end;

thus ( X is filtered Subset of S implies X is filtered Subset of L ) :: thesis: verum

proof

assume A5: X is filtered Subset of S ; :: thesis: X is filtered Subset of L
the carrier of S c= the carrier of L by YELLOW_0:def 13;
then reconsider X = X as Subset of L by A5, XBOOLE_1:1;
for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y )

proof

let x, y be Element of L; :: thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume A6: ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
then reconsider x' = x, y' = y as Element of S by A5;
consider z being Element of S such that
A7: z in X and
A8: ( z <= x' & z <= y' ) by A5, A6, WAYBEL_0:def 2;
reconsider z = z as Element of L by YELLOW_0:59;
take z ; :: thesis: ( z in X & z <= x & z <= y )
thus ( z in X & z <= x & z <= y ) by A7, A8, YELLOW_0:60; :: thesis: verum

end;

hence X is filtered Subset of L by WAYBEL_0:def 2; :: thesis: verum

end;