let S1, S2 be non empty reflexive RelStr ; :: thesis: for D being non empty directed Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= downarrow D
let D be non empty directed Subset of [:S1,S2:]; :: thesis: [:(proj1 D),(proj2 D):] c= downarrow D
set D1 = proj1 D;
set D2 = proj2 D;
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set ;
reconsider D' = D as non empty Subset of [:C1,C2:] by Def2;
A1: D' c= [:(proj1 D),(proj2 D):] by Th1;
not proj1 D' is empty ;
then reconsider D1 = proj1 D as non empty Subset of S1 ;
not proj2 D' is empty ;
then reconsider D2 = proj2 D as non empty Subset of S2 ;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in [:(proj1 D),(proj2 D):] or q in downarrow D )
assume q in [:(proj1 D),(proj2 D):] ; :: thesis: q in downarrow D
then consider d, e being set such that
A2: ( d in D1 & e in D2 & q = [d,e] ) by ZFMISC_1:def 2;
A3: downarrow 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:14;
consider y being set such that
A4: [d,y] in D by A2, RELAT_1:def 4;
consider x being set such that
A5: [x,e] in D by A2, RELAT_1:def 5;
reconsider x = x, d = d as Element of D1 by A4, A5, FUNCT_5:4;
reconsider y = y, e = e as Element of D2 by A4, A5, FUNCT_5:4;
consider z being Element of [:S1,S2:] such that
A6: ( z in D & [d,y] <= z & [x,e] <= z ) by A4, A5, WAYBEL_0:def 1;
consider z1, z2 being set such that
A7: ( z1 in D1 & z2 in D2 & z = [z1,z2] ) by A1, A6, ZFMISC_1:def 2;
reconsider z1 = z1 as Element of D1 by A7;
reconsider z2 = z2 as Element of D2 by A7;
( d <= z1 & e <= z2 ) by A6, A7, Th11;
then [d,e] <= [z1,z2] by Th11;
hence q in downarrow D by A2, A3, A6, A7; :: thesis: verum