let S1, S2 be non empty reflexive RelStr ; :: thesis: for D being non empty filtered Subset of [:S1,S2:] holds
( proj1 D is filtered & proj2 D is filtered )
let D be non empty filtered Subset of [:S1,S2:]; :: thesis: ( proj1 D is filtered & proj2 D is filtered )
set D1 = proj1 D;
set D2 = proj2 D;
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then A1: D c= [:(proj1 D),(proj2 D):] by Th1;
thus proj1 D is filtered :: thesis: proj2 D is filtered

proof

let x, y be Element of S1; :: according to WAYBEL_0:def 2 :: thesis: ( not x in proj1 D or not y in proj1 D or ex b₁ being Element of the carrier of S1 st
( b₁ in proj1 D & b₁ <= x & b₁ <= y ) )
assume that
A2: x in proj1 D and
A3: y in proj1 D ; :: thesis: ex b₁ being Element of the carrier of S1 st
( b₁ in proj1 D & b₁ <= x & b₁ <= y )
consider q2 being object such that
A4: [y,q2] in D by A3, XTUPLE_0:def 12;
reconsider D29 = proj2 D as non empty Subset of S2 by A2, FUNCT_5:16;
reconsider D19 = proj1 D as non empty Subset of S1 by A2;
consider q1 being object such that
A5: [x,q1] in D by A2, XTUPLE_0:def 12;
reconsider q2 = q2 as Element of D29 by A4, XTUPLE_0:def 13;
reconsider q1 = q1 as Element of D29 by A5, XTUPLE_0:def 13;
consider z being Element of [:S1,S2:] such that
A6: z in D and
A7: ( [x,q1] >= z & [y,q2] >= z ) by A5, A4, WAYBEL_0:def 2;
reconsider z2 = z `2 as Element of D29 by A1, A6, MCART_1:10;
reconsider zz = z `1 as Element of D19 by A1, A6, MCART_1:10;
take zz ; :: thesis: ( zz in proj1 D & zz <= x & zz <= y )
thus zz in proj1 D ; :: thesis: ( zz <= x & zz <= y )
ex x, y being object st
( x in D19 & y in D29 & z = [x,y] ) by A1, A6, ZFMISC_1:def 2;
then z = [zz,z2] ;
hence ( zz <= x & zz <= y ) by A7, Th11; :: thesis: verum

end;

let x, y be Element of S2; :: according to WAYBEL_0:def 2 :: thesis: ( not x in proj2 D or not y in proj2 D or ex b₁ being Element of the carrier of S2 st
( b₁ in proj2 D & b₁ <= x & b₁ <= y ) )
assume that
A8: x in proj2 D and
A9: y in proj2 D ; :: thesis: ex b₁ being Element of the carrier of S2 st
( b₁ in proj2 D & b₁ <= x & b₁ <= y )
consider q2 being object such that
A10: [q2,y] in D by A9, XTUPLE_0:def 13;
reconsider D29 = proj2 D as non empty Subset of S2 by A8;
reconsider D19 = proj1 D as non empty Subset of S1 by A8, FUNCT_5:16;
consider q1 being object such that
A11: [q1,x] in D by A8, XTUPLE_0:def 13;
reconsider q2 = q2 as Element of D19 by A10, XTUPLE_0:def 12;
reconsider q1 = q1 as Element of D19 by A11, XTUPLE_0:def 12;
consider z being Element of [:S1,S2:] such that
A12: z in D and
A13: ( [q1,x] >= z & [q2,y] >= z ) by A11, A10, WAYBEL_0:def 2;
reconsider z2 = z `1 as Element of D19 by A1, A12, MCART_1:10;
reconsider zz = z `2 as Element of D29 by A1, A12, MCART_1:10;
take zz ; :: thesis: ( zz in proj2 D & zz <= x & zz <= y )
thus zz in proj2 D ; :: thesis: ( zz <= x & zz <= y )
ex x, y being object st
( x in D19 & y in D29 & z = [x,y] ) by A1, A12, ZFMISC_1:def 2;
then z = [z2,zz] ;
hence ( zz <= x & zz <= y ) by A13, Th11; :: thesis: verum