set X = [:D1,D2:];
[:D1,D2:] is upper
proof
let x,
y be
Element of
[:S1,S2:];
WAYBEL_0:def 20 ( not x in [:D1,D2:] or not x <= y or y in [:D1,D2:] )
assume that A1:
x in [:D1,D2:]
and A2:
x <= y
;
y in [:D1,D2:]
consider x1,
x2 being
object such that A3:
x1 in D1
and A4:
x2 in D2
and A5:
x = [x1,x2]
by A1, ZFMISC_1:def 2;
reconsider s1 =
S1,
s2 =
S2 as non
empty RelStr by A3, A4;
set C1 = the
carrier of
s1;
set C2 = the
carrier of
s2;
the
carrier of
[:S1,S2:] = [: the carrier of s1, the carrier of s2:]
by Def2;
then consider y1,
y2 being
object such that A6:
y1 in the
carrier of
s1
and A7:
y2 in the
carrier of
s2
and A8:
y = [y1,y2]
by ZFMISC_1:def 2;
reconsider x2 =
x2,
y2 =
y2 as
Element of
s2 by A4, A7;
x2 <= y2
by A2, A3, A5, A6, A8, Th11;
then A9:
y2 in D2
by A4, WAYBEL_0:def 20;
reconsider x1 =
x1,
y1 =
y1 as
Element of
s1 by A3, A6;
x1 <= y1
by A2, A4, A5, A7, A8, Th11;
then
y1 in D1
by A3, WAYBEL_0:def 20;
hence
y in [:D1,D2:]
by A8, A9, ZFMISC_1:87;
verum
end;
hence
for b1 being Subset of [:S1,S2:] st b1 = [:D1,D2:] holds
b1 is upper
; verum