let S, T be RelStr ; for X being Subset of S
for Y being Subset of T holds [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]
let X be Subset of S; for Y being Subset of T holds [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]
let Y be Subset of T; [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]
hereby TARSKI:def 3,
XBOOLE_0:def 10 downarrow [:X,Y:] c= [:(downarrow X),(downarrow Y):]
let x be
object ;
( x in [:(downarrow X),(downarrow Y):] implies x in downarrow [:X,Y:] )assume
x in [:(downarrow X),(downarrow Y):]
;
x in downarrow [:X,Y:]then consider x1,
x2 being
object such that A1:
x1 in downarrow X
and A2:
x2 in downarrow Y
and A3:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider S9 =
S,
T9 =
T as non
empty RelStr by A1, A2;
reconsider x1 =
x1 as
Element of
S9 by A1;
consider y1 being
Element of
S9 such that A4:
(
y1 >= x1 &
y1 in X )
by A1, WAYBEL_0:def 15;
reconsider x2 =
x2 as
Element of
T9 by A2;
consider y2 being
Element of
T9 such that A5:
(
y2 >= x2 &
y2 in Y )
by A2, WAYBEL_0:def 15;
(
[y1,y2] in [:X,Y:] &
[y1,y2] >= [x1,x2] )
by A4, A5, YELLOW_3:11, ZFMISC_1:87;
hence
x in downarrow [:X,Y:]
by A3, WAYBEL_0:def 15;
verum
end;
let x be object ; TARSKI:def 3 ( not x in downarrow [:X,Y:] or x in [:(downarrow X),(downarrow Y):] )
assume A6:
x in downarrow [:X,Y:]
; x in [:(downarrow X),(downarrow Y):]
A7:
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then
ex a, b being object st
( a in the carrier of S & b in the carrier of T & x = [a,b] )
by A6, ZFMISC_1:def 2;
then reconsider S9 = S, T9 = T as non empty RelStr ;
reconsider x9 = x as Element of [:S9,T9:] by A6;
consider y being Element of [:S9,T9:] such that
A8:
( y >= x9 & y in [:X,Y:] )
by A6, WAYBEL_0:def 15;
( y `2 >= x9 `2 & y `2 in Y )
by A8, MCART_1:10, YELLOW_3:12;
then A9:
x `2 in downarrow Y
by WAYBEL_0:def 15;
( y `1 >= x9 `1 & y `1 in X )
by A8, MCART_1:10, YELLOW_3:12;
then A10:
x `1 in downarrow X
by WAYBEL_0:def 15;
x9 = [(x9 `1),(x9 `2)]
by A7, MCART_1:21;
hence
x in [:(downarrow X),(downarrow Y):]
by A10, A9, ZFMISC_1:def 2; verum