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 x9 = x, y9 = y as Element of S by A1;
consider z being Element of S such that
A3: ( z in X & x9 <= z & y9 <= z ) by A1, A2, WAYBEL_0:def 1;
reconsider z = z as Element of L by YELLOW_0:58;
take z ; :: thesis: ( z in X & x <= z & y <= z )
thus ( z in X & x <= z & y <= z ) by A3, YELLOW_0:59; :: 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 A4: 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 A4, 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 A5: ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
then reconsider x9 = x, y9 = y as Element of S by A4;
consider z being Element of S such that
A6: ( z in X & z <= x9 & z <= y9 ) by A4, A5, WAYBEL_0:def 2;
reconsider z = z as Element of L by YELLOW_0:58;
take z ; :: thesis: ( z in X & z <= x & z <= y )
thus ( z in X & z <= x & z <= y ) by A6, YELLOW_0:59; :: thesis: verum

end;

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

end;