set X = [:D1,D2:];
[:D1,D2:] is lower

proof

let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def 19 :: thesis: ( not x in [:D1,D2:] or not y <= x or y in [:D1,D2:] )
assume that
A1: x in [:D1,D2:] and
A2: x >= y ; :: thesis: 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 19;
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 19;
hence y in [:D1,D2:] by A8, A9, ZFMISC_1:87; :: thesis: verum

end;

hence for b₁ being Subset of [:S1,S2:] st b₁ = [:D1,D2:] holds
b₁ is lower ; :: thesis: verum