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 implies X is directed Subset of ) & ( X is filtered Subset of implies X is filtered Subset of ) )
let L be non empty RelStr ; :: thesis: for S being non empty SubRelStr of L holds
( ( X is directed Subset of implies X is directed Subset of ) & ( X is filtered Subset of implies X is filtered Subset of ) )
let S be non empty SubRelStr of L; :: thesis: ( ( X is directed Subset of implies X is directed Subset of ) & ( X is filtered Subset of implies X is filtered Subset of ) )
thus ( X is directed Subset of implies X is directed Subset of ) :: thesis: ( X is filtered Subset of implies X is filtered Subset of )

proof

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

proof

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

end;

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

end;

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

proof

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

proof

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

end;

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

end;