let S1, S2 be non empty reflexive RelStr ; for D being non empty directed Subset of [:S1,S2:] holds
( proj1 D is directed & proj2 D is directed )
let D be non empty directed Subset of [:S1,S2:]; ( proj1 D is directed & proj2 D is directed )
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 directed
proj2 D is directed proof
let x,
y be
Element of
S1;
WAYBEL_0:def 1 ( not x in proj1 D or not y in proj1 D or ex b1 being Element of the carrier of S1 st
( b1 in proj1 D & x <= b1 & y <= b1 ) )
assume that A2:
x in proj1 D
and A3:
y in proj1 D
;
ex b1 being Element of the carrier of S1 st
( b1 in proj1 D & x <= b1 & y <= b1 )
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 1;
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
;
( zz in proj1 D & x <= zz & y <= zz )
thus
zz in proj1 D
;
( x <= zz & y <= zz )
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
(
x <= zz &
y <= zz )
by A7, Th11;
verum
end;
let x, y be Element of S2; WAYBEL_0:def 1 ( not x in proj2 D or not y in proj2 D or ex b1 being Element of the carrier of S2 st
( b1 in proj2 D & x <= b1 & y <= b1 ) )
assume that
A8:
x in proj2 D
and
A9:
y in proj2 D
; ex b1 being Element of the carrier of S2 st
( b1 in proj2 D & x <= b1 & y <= b1 )
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 1;
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
; ( zz in proj2 D & x <= zz & y <= zz )
thus
zz in proj2 D
; ( x <= zz & y <= zz )
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
( x <= zz & y <= zz )
by A13, Th11; verum