let L1, L2 be RelStr ; ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered )
assume A1:
RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #)
; for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered
let X1 be Subset of L1; for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered
let X2 be Subset of L2; ( X1 = X2 & X1 is filtered implies X2 is filtered )
assume A2:
X1 = X2
; ( not X1 is filtered or X2 is filtered )
assume A3:
for x, y being Element of L1 st x in X1 & y in X1 holds
ex z being Element of L1 st
( z in X1 & x >= z & y >= z )
; WAYBEL_0:def 2 X2 is filtered
let x, y be Element of L2; WAYBEL_0:def 2 ( x in X2 & y in X2 implies ex z being Element of L2 st
( z in X2 & z <= x & z <= y ) )
reconsider x9 = x, y9 = y as Element of L1 by A1;
assume that
A4:
x in X2
and
A5:
y in X2
; ex z being Element of L2 st
( z in X2 & z <= x & z <= y )
consider z9 being Element of L1 such that
A6:
z9 in X1
and
A7:
x9 >= z9
and
A8:
y9 >= z9
by A2, A3, A4, A5;
reconsider z = z9 as Element of L2 by A1;
take
z
; ( z in X2 & z <= x & z <= y )
thus
( z in X2 & z <= x & z <= y )
by A1, A2, A6, A7, A8, YELLOW_0:1; verum