let S1, S2 be non empty RelStr ; for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds
( D1 is filtered & D2 is filtered )
let D1 be non empty Subset of S1; for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds
( D1 is filtered & D2 is filtered )
let D2 be non empty Subset of S2; ( [:D1,D2:] is filtered implies ( D1 is filtered & D2 is filtered ) )
assume A1:
[:D1,D2:] is filtered
; ( D1 is filtered & D2 is filtered )
thus
D1 is filtered
D2 is filtered proof
set q1 = the
Element of
D2;
let x,
y be
Element of
S1;
WAYBEL_0:def 2 ( not x in D1 or not y in D1 or ex b1 being Element of the carrier of S1 st
( b1 in D1 & b1 <= x & b1 <= y ) )
assume
(
x in D1 &
y in D1 )
;
ex b1 being Element of the carrier of S1 st
( b1 in D1 & b1 <= x & b1 <= y )
then
(
[x, the Element of D2] in [:D1,D2:] &
[y, the Element of D2] in [:D1,D2:] )
by ZFMISC_1:87;
then consider z being
Element of
[:S1,S2:] such that A2:
z in [:D1,D2:]
and A3:
(
[x, the Element of D2] >= z &
[y, the Element of D2] >= z )
by A1;
reconsider z2 =
z `2 as
Element of
D2 by A2, MCART_1:10;
reconsider zz =
z `1 as
Element of
D1 by A2, MCART_1:10;
take
zz
;
( zz in D1 & zz <= x & zz <= y )
thus
zz in D1
;
( zz <= x & zz <= y )
ex
x,
y being
object st
(
x in D1 &
y in D2 &
z = [x,y] )
by A2, ZFMISC_1:def 2;
then
(
[x, the Element of D2] >= [zz,z2] &
[y, the Element of D2] >= [zz,z2] )
by A3;
hence
(
zz <= x &
zz <= y )
by Th11;
verum
end;
set q1 = the Element of D1;
let x, y be Element of S2; WAYBEL_0:def 2 ( not x in D2 or not y in D2 or ex b1 being Element of the carrier of S2 st
( b1 in D2 & b1 <= x & b1 <= y ) )
assume
( x in D2 & y in D2 )
; ex b1 being Element of the carrier of S2 st
( b1 in D2 & b1 <= x & b1 <= y )
then
( [ the Element of D1,x] in [:D1,D2:] & [ the Element of D1,y] in [:D1,D2:] )
by ZFMISC_1:87;
then consider z being Element of [:S1,S2:] such that
A4:
z in [:D1,D2:]
and
A5:
( [ the Element of D1,x] >= z & [ the Element of D1,y] >= z )
by A1;
reconsider z2 = z `1 as Element of D1 by A4, MCART_1:10;
reconsider zz = z `2 as Element of D2 by A4, MCART_1:10;
take
zz
; ( zz in D2 & zz <= x & zz <= y )
thus
zz in D2
; ( zz <= x & zz <= y )
ex x, y being object st
( x in D1 & y in D2 & z = [x,y] )
by A4, ZFMISC_1:def 2;
then
( [ the Element of D1,x] >= [z2,zz] & [ the Element of D1,y] >= [z2,zz] )
by A5;
hence
( zz <= x & zz <= y )
by Th11; verum