let S1, S2 be non empty reflexive RelStr ; for D being non empty upper Subset of [:S1,S2:] holds
( proj1 D is upper & proj2 D is upper )
let D be non empty upper Subset of [:S1,S2:]; ( proj1 D is upper & proj2 D is upper )
set D1 = proj1 D;
set D2 = proj2 D;
reconsider d1 = proj1 D as non empty Subset of S1 by Th21;
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 upper
proj2 D is upper proof
reconsider d2 =
proj2 D as non
empty Subset of
S2 by Th21;
let x,
y be
Element of
S1;
WAYBEL_0:def 20 ( not x in proj1 D or not x <= y or y in proj1 D )
assume that A2:
x in proj1 D
and A3:
x <= y
;
y in proj1 D
consider q1 being
object such that A4:
[x,q1] in D
by A2, XTUPLE_0:def 12;
reconsider q1 =
q1 as
Element of
d2 by A1, A4, ZFMISC_1:87;
q1 <= q1
;
then
[x,q1] <= [y,q1]
by A3, Th11;
then
[y,q1] in D
by A4, WAYBEL_0:def 20;
hence
y in proj1 D
by A1, ZFMISC_1:87;
verum
end;
let x, y be Element of S2; WAYBEL_0:def 20 ( not x in proj2 D or not x <= y or y in proj2 D )
assume that
A5:
x in proj2 D
and
A6:
x <= y
; y in proj2 D
consider q1 being object such that
A7:
[q1,x] in D
by A5, XTUPLE_0:def 13;
reconsider q1 = q1 as Element of d1 by A1, A7, ZFMISC_1:87;
q1 <= q1
;
then
[q1,x] <= [q1,y]
by A6, Th11;
then
[q1,y] in D
by A7, WAYBEL_0:def 20;
hence
y in proj2 D
by A1, ZFMISC_1:87; verum