let S1, S2 be non empty reflexive RelStr ; :: thesis: for D being non empty filtered Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= uparrow D
let D be non empty filtered Subset of [:S1,S2:]; :: thesis: [:(proj1 D),(proj2 D):] c= uparrow D
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set ;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in [:(proj1 D),(proj2 D):] or q in uparrow D )
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
set D1 = proj1 D;
set D2 = proj2 D;
A1: uparrow D = { x where x is Element of [:S1,S2:] : ex y being Element of [:S1,S2:] st
( x >= y & y in D ) } by WAYBEL_0:15;
A2: D9 c= [:(proj1 D),(proj2 D):] by Th1;
not proj2 D9 is empty ;
then reconsider D2 = proj2 D as non empty Subset of S2 ;
not proj1 D9 is empty ;
then reconsider D1 = proj1 D as non empty Subset of S1 ;
assume q in [:(proj1 D),(proj2 D):] ; :: thesis: q in uparrow D
then consider d, e being object such that
A3: d in D1 and
A4: e in D2 and
A5: q = [d,e] by ZFMISC_1:def 2;
consider y being object such that
A6: [d,y] in D by A3, XTUPLE_0:def 12;
consider x being object such that
A7: [x,e] in D by A4, XTUPLE_0:def 13;
reconsider y = y, e = e as Element of D2 by A6, A7, XTUPLE_0:def 13;
reconsider x = x, d = d as Element of D1 by A6, A7, XTUPLE_0:def 12;
consider z being Element of [:S1,S2:] such that
A8: z in D and
A9: ( [d,y] >= z & [x,e] >= z ) by A6, A7, WAYBEL_0:def 2;
consider z1, z2 being object such that
A10: z1 in D1 and
A11: z2 in D2 and
A12: z = [z1,z2] by A2, A8, ZFMISC_1:def 2;
reconsider z2 = z2 as Element of D2 by A11;
reconsider z1 = z1 as Element of D1 by A10;
( d >= z1 & e >= z2 ) by A9, A10, A11, A12, Th11;
then [d,e] >= [z1,z2] by Th11;
hence q in uparrow D by A5, A1, A8, A12; :: thesis: verum