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 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; :: thesis: ( 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
; :: thesis: 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; :: thesis: ( 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; :: thesis: 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; :: 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: verumproof
let x,
y be
Element of
S2;
:: according to WAYBEL_0:def 2 :: thesis: ( 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 )
;
:: thesis: ex b1 being Element of the carrier of S2 st
( b1 in X2 & b1 <= x & b1 <= y )
then reconsider x' =
x,
y' =
y as
Element of
S1 by A2;
consider z being
Element of
S1 such that A5:
(
z in X &
z <= x' &
z <= y' )
by A2, A3, A4, WAYBEL_0:def 2;
reconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of
L by YELLOW_0:59;
reconsider z =
z as
Element of
S2 by A2, A5;
take
z
;
:: thesis: ( z in X2 & z <= x & z <= y )
(
z1 <= x1 &
z1 <= y1 )
by A5, YELLOW_0:60;
hence
(
z in X2 &
z <= x &
z <= y )
by A2, A5, YELLOW_0:61;
:: thesis: verum
end;
end;
assume A6:
X is directed
; :: thesis: X2 is directed
let x, y be Element of S2; :: according to WAYBEL_0:def 1 :: thesis: ( 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 A7:
( x in X2 & y in X2 )
; :: thesis: ex b1 being Element of the carrier of S2 st
( b1 in X2 & x <= b1 & y <= b1 )
then reconsider x' = x, y' = y as Element of S1 by A2;
consider z being Element of S1 such that
A8:
( z in X & x' <= z & y' <= z )
by A2, A6, A7, WAYBEL_0:def 1;
reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:59;
reconsider z = z as Element of S2 by A2, A8;
take
z
; :: thesis: ( z in X2 & x <= z & y <= z )
( x1 <= z1 & y1 <= z1 )
by A8, YELLOW_0:60;
hence
( z in X2 & x <= z & y <= z )
by A2, A8, YELLOW_0:61; :: thesis: verum