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 b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 ) )
assume that
A3: x in X and
A4: y in X ; :: thesis: ex b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 )
x in the carrier of S by A3;
then reconsider x9 = x, y9 = y as Element of L by A2;
consider z being Element of L such that
A5: z in X and
A6: z >= x9 and
A7: z >= y9 by A1, A3, A4, WAYBEL_0:def 1;
reconsider z = z as Element of S by A5;
take z ; :: thesis: ( z in X & x <= z & y <= z )
thus ( z in X & x <= z & y <= z ) by A5, A6, A7, YELLOW_0:60; :: thesis: verum
end;
end;
assume A8: X is filtered Subset of L ; :: thesis: X is filtered
A9: 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 b1 being Element of the carrier of S st
( b1 in X & b1 <= x & b1 <= y ) )
assume that
A10: x in X and
A11: y in X ; :: thesis: ex b1 being Element of the carrier of S st
( b1 in X & b1 <= x & b1 <= y )
x in the carrier of S by A10;
then reconsider x9 = x, y9 = y as Element of L by A9;
consider z being Element of L such that
A12: z in X and
A13: z <= x9 and
A14: z <= y9 by A8, A10, A11, WAYBEL_0:def 2;
reconsider z = z as Element of S by A12;
take z ; :: thesis: ( z in X & z <= x & z <= y )
thus ( z in X & z <= x & z <= y ) by A12, A13, A14, YELLOW_0:60; :: thesis: verum