let S, T be RelStr ; for X being Subset of S
for Y being Subset of T holds [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]
let X be Subset of S; for Y being Subset of T holds [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]
let Y be Subset of T; [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]
hereby TARSKI:def 3,
XBOOLE_0:def 10 uparrow [:X,Y:] c= [:(uparrow X),(uparrow Y):]
let x be
object ;
( x in [:(uparrow X),(uparrow Y):] implies x in uparrow [:X,Y:] )assume
x in [:(uparrow X),(uparrow Y):]
;
x in uparrow [:X,Y:]then consider x1,
x2 being
object such that A1:
x1 in uparrow X
and A2:
x2 in uparrow 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 16;
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 16;
(
[y1,y2] in [:X,Y:] &
[y1,y2] <= [x1,x2] )
by A4, A5, YELLOW_3:11, ZFMISC_1:87;
hence
x in uparrow [:X,Y:]
by A3, WAYBEL_0:def 16;
verum
end;
let x be object ; TARSKI:def 3 ( not x in uparrow [:X,Y:] or x in [:(uparrow X),(uparrow Y):] )
assume A6:
x in uparrow [:X,Y:]
; x in [:(uparrow X),(uparrow 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 16;
( y `2 <= x9 `2 & y `2 in Y )
by A8, MCART_1:10, YELLOW_3:12;
then A9:
x `2 in uparrow Y
by WAYBEL_0:def 16;
( y `1 <= x9 `1 & y `1 in X )
by A8, MCART_1:10, YELLOW_3:12;
then A10:
x `1 in uparrow X
by WAYBEL_0:def 16;
x9 = [(x9 `1),(x9 `2)]
by A7, MCART_1:21;
hence
x in [:(uparrow X),(uparrow Y):]
by A10, A9, ZFMISC_1:def 2; verum