let S1, S2 be non empty RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( [:D1,D2:] is filtered implies ( D1 is filtered & D2 is filtered ) )
assume A1: [:D1,D2:] is filtered ; :: thesis: ( D1 is filtered & D2 is filtered )
thus D1 is filtered :: thesis: D2 is filtered

proof

set q1 = the Element of D2;
let x, y be Element of S1; :: according to WAYBEL_0:def 2 :: thesis: ( not x in D1 or not y in D1 or ex b₁ being Element of the carrier of S1 st
( b₁ in D1 & b₁ <= x & b₁ <= y ) )
assume ( x in D1 & y in D1 ) ; :: thesis: ex b₁ being Element of the carrier of S1 st
( b₁ in D1 & b₁ <= x & b₁ <= 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 ; :: thesis: ( zz in D1 & zz <= x & zz <= y )
thus zz in D1 ; :: thesis: ( 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; :: thesis: verum

end;

set q1 = the Element of D1;
let x, y be Element of S2; :: according to WAYBEL_0:def 2 :: thesis: ( not x in D2 or not y in D2 or ex b₁ being Element of the carrier of S2 st
( b₁ in D2 & b₁ <= x & b₁ <= y ) )
assume ( x in D2 & y in D2 ) ; :: thesis: ex b₁ being Element of the carrier of S2 st
( b₁ in D2 & b₁ <= x & b₁ <= 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 ; :: thesis: ( zz in D2 & zz <= x & zz <= y )
thus zz in D2 ; :: thesis: ( 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; :: thesis: verum