set X = [:D1,D2:];
[:D1,D2:] is upper
proof
let x,
y be
Element of
[:S1,S2:];
:: according to WAYBEL_0:def 20 :: thesis: ( not x in [:D1,D2:] or not x <= y or y in [:D1,D2:] )
assume A1:
(
x in [:D1,D2:] &
x <= y )
;
:: thesis: y in [:D1,D2:]
then consider x1,
x2 being
set such that A2:
(
x1 in D1 &
x2 in D2 &
x = [x1,x2] )
by ZFMISC_1:def 2;
reconsider s1 =
S1,
s2 =
S2 as non
empty RelStr by A2;
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
set such that A3:
(
y1 in the
carrier of
s1 &
y2 in the
carrier of
s2 &
y = [y1,y2] )
by ZFMISC_1:def 2;
reconsider x1 =
x1,
y1 =
y1 as
Element of
s1 by A2, A3;
reconsider x2 =
x2,
y2 =
y2 as
Element of
s2 by A2, A3;
(
x1 <= y1 &
x2 <= y2 )
by A1, A2, A3, Th11;
then
(
y1 in D1 &
y2 in D2 )
by A2, WAYBEL_0:def 20;
hence
y in [:D1,D2:]
by A3, ZFMISC_1:106;
:: thesis: verum
end;
hence
[:D1,D2:] is upper Subset of [:S1,S2:]
; :: thesis: verum