let L be non empty RelStr ; :: thesis: for S, T being non empty full SubRelStr of L st the carrier of S c= the carrier of T holds
for X being Subset of holds
( X is Subset of & ( for Y being Subset of st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
let S1, S2 be non empty full SubRelStr of L; :: thesis: ( the carrier of S1 c= the carrier of S2 implies for X being Subset of holds
( X is Subset of & ( for Y being Subset of st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) ) )
assume A1: the carrier of S1 c= the carrier of S2 ; :: thesis: for X being Subset of holds
( X is Subset of & ( for Y being Subset of st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
let X be Subset of ; :: thesis: ( X is Subset of & ( for Y being Subset of st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
thus X is Subset of by A1, XBOOLE_1:1; :: thesis: for Y being Subset of st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) )
let X2 be Subset of ; :: thesis: ( X = X2 implies ( ( X is filtered implies X2 is filtered ) & ( X is directed implies X2 is directed ) ) )
assume A2: X = X2 ; :: thesis: ( ( X is filtered implies X2 is filtered ) & ( X is directed implies X2 is directed ) )

hereby :: thesis: ( X is directed implies X2 is directed )

assume A3: X is filtered ; :: thesis: X2 is filtered
thus X2 is filtered :: thesis: verum

proof

let x, y be Element of ; :: according to WAYBEL_0:def 2 :: thesis: ( not x in X2 or not y in X2 or ex b₁ being Element of the carrier of S2 st
( b₁ in X2 & b₁ <= x & b₁ <= y ) )
assume A4: ( x in X2 & y in X2 ) ; :: thesis: ex b₁ being Element of the carrier of S2 st
( b₁ in X2 & b₁ <= x & b₁ <= y )
then reconsider x' = x, y' = y as Element of by A2;
consider z being Element of such that
A5: z in X and
A6: ( z <= x' & z <= y' ) by A2, A3, A4, WAYBEL_0:def 2;
reconsider x1 = x, y1 = y, z1 = z as Element of by YELLOW_0:59;
reconsider z = z as Element of by A2, A5;
take z ; :: thesis: ( z in X2 & z <= x & z <= y )
( z1 <= x1 & z1 <= y1 ) by A6, YELLOW_0:60;
hence ( z in X2 & z <= x & z <= y ) by A2, A5, YELLOW_0:61; :: thesis: verum

end;

end;

assume A7: X is directed ; :: thesis: X2 is directed
let x, y be Element of ; :: according to WAYBEL_0:def 1 :: thesis: ( not x in X2 or not y in X2 or ex b₁ being Element of the carrier of S2 st
( b₁ in X2 & x <= b₁ & y <= b₁ ) )
assume A8: ( x in X2 & y in X2 ) ; :: thesis: ex b₁ being Element of the carrier of S2 st
( b₁ in X2 & x <= b₁ & y <= b₁ )
then reconsider x' = x, y' = y as Element of by A2;
consider z being Element of such that
A9: z in X and
A10: ( x' <= z & y' <= z ) by A2, A7, A8, WAYBEL_0:def 1;
reconsider x1 = x, y1 = y, z1 = z as Element of by YELLOW_0:59;
reconsider z = z as Element of by A2, A9;
take z ; :: thesis: ( z in X2 & x <= z & y <= z )
( x1 <= z1 & y1 <= z1 ) by A10, YELLOW_0:60;
hence ( z in X2 & x <= z & y <= z ) by A2, A9, YELLOW_0:61; :: thesis: verum