let S1, S2 be non empty reflexive RelStr ; 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:]; [:(proj1 D),(proj2 D):] c= downarrow D
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set ;
let q be object ; TARSKI:def 3 ( not q in [:(proj1 D),(proj2 D):] or q in downarrow D )
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
set D1 = proj1 D;
set D2 = proj2 D;
A1:
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;
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):]
; q in downarrow 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 1;
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 downarrow D
by A5, A1, A8, A12; verum