let L be non empty RelStr ; 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 S holds
( X is Subset of T & ( for Y being Subset of T 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; ( the carrier of S1 c= the carrier of S2 implies for X being Subset of S1 holds
( X is Subset of S2 & ( for Y being Subset of S2 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
; for X being Subset of S1 holds
( X is Subset of S2 & ( for Y being Subset of S2 st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
let X be Subset of S1; ( X is Subset of S2 & ( for Y being Subset of S2 st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
thus
X is Subset of S2
by A1, XBOOLE_1:1; for Y being Subset of S2 st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) )
let X2 be Subset of S2; ( X = X2 implies ( ( X is filtered implies X2 is filtered ) & ( X is directed implies X2 is directed ) ) )
assume A2:
X = X2
; ( ( X is filtered implies X2 is filtered ) & ( X is directed implies X2 is directed ) )
hereby ( X is directed implies X2 is directed )
assume A3:
X is
filtered
;
X2 is filtered thus
X2 is
filtered
verumproof
let x,
y be
Element of
S2;
WAYBEL_0:def 2 ( not x in X2 or not y in X2 or ex b1 being Element of the carrier of S2 st
( b1 in X2 & b1 <= x & b1 <= y ) )
assume A4:
(
x in X2 &
y in X2 )
;
ex b1 being Element of the carrier of S2 st
( b1 in X2 & b1 <= x & b1 <= y )
then reconsider x9 =
x,
y9 =
y as
Element of
S1 by A2;
consider z being
Element of
S1 such that A5:
z in X
and A6:
(
z <= x9 &
z <= y9 )
by A2, A3, A4;
reconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of
L by YELLOW_0:58;
reconsider z =
z as
Element of
S2 by A2, A5;
take
z
;
( z in X2 & z <= x & z <= y )
(
z1 <= x1 &
z1 <= y1 )
by A6, YELLOW_0:59;
hence
(
z in X2 &
z <= x &
z <= y )
by A2, A5, YELLOW_0:60;
verum
end;
end;
assume A7:
X is directed
; X2 is directed
let x, y be Element of S2; WAYBEL_0:def 1 ( not x in X2 or not y in X2 or ex b1 being Element of the carrier of S2 st
( b1 in X2 & x <= b1 & y <= b1 ) )
assume A8:
( x in X2 & y in X2 )
; ex b1 being Element of the carrier of S2 st
( b1 in X2 & x <= b1 & y <= b1 )
then reconsider x9 = x, y9 = y as Element of S1 by A2;
consider z being Element of S1 such that
A9:
z in X
and
A10:
( x9 <= z & y9 <= z )
by A2, A7, A8;
reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:58;
reconsider z = z as Element of S2 by A2, A9;
take
z
; ( z in X2 & x <= z & y <= z )
( x1 <= z1 & y1 <= z1 )
by A10, YELLOW_0:59;
hence
( z in X2 & x <= z & y <= z )
by A2, A9, YELLOW_0:60; verum