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

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 A2: ( x in D1 & y in D1 ) ; :: thesis: ex b₁ being Element of the carrier of S1 st
( b₁ in D1 & b₁ <= x & b₁ <= y )
consider q1 being Element of D2;
( [x,q1] in [:D1,D2:] & [y,q1] in [:D1,D2:] ) by A2, ZFMISC_1:106;
then consider z being Element of [:S1,S2:] such that
A3: ( z in [:D1,D2:] & [x,q1] >= z & [y,q1] >= z ) by A1, WAYBEL_0:def 2;
reconsider zz = z `1 as Element of D1 by A3, MCART_1:10;
reconsider z2 = z `2 as Element of D2 by A3, 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 set st
( x in D1 & y in D2 & z = [x,y] ) by A3, ZFMISC_1:def 2;
then ( [x,q1] >= [zz,z2] & [y,q1] >= [zz,z2] ) by A3, MCART_1:8;
hence ( zz <= x & zz <= y ) by Th11; :: thesis: verum

end;

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 A4: ( x in D2 & y in D2 ) ; :: thesis: ex b₁ being Element of the carrier of S2 st
( b₁ in D2 & b₁ <= x & b₁ <= y )
consider q1 being Element of D1;
( [q1,x] in [:D1,D2:] & [q1,y] in [:D1,D2:] ) by A4, ZFMISC_1:106;
then consider z being Element of [:S1,S2:] such that
A5: ( z in [:D1,D2:] & [q1,x] >= z & [q1,y] >= z ) by A1, WAYBEL_0:def 2;
reconsider zz = z `2 as Element of D2 by A5, MCART_1:10;
reconsider z2 = z `1 as Element of D1 by A5, 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 set st
( x in D1 & y in D2 & z = [x,y] ) by A5, ZFMISC_1:def 2;
then ( [q1,x] >= [z2,zz] & [q1,y] >= [z2,zz] ) by A5, MCART_1:8;
hence ( zz <= x & zz <= y ) by Th11; :: thesis: verum