let S, T be non empty RelStr ; for s being Element of S
for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]
let s be Element of S; for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]
let t be Element of T; [:(downarrow s),(downarrow t):] = downarrow [s,t]
hereby TARSKI:def 3,
XBOOLE_0:def 10 downarrow [s,t] c= [:(downarrow s),(downarrow t):]
let x be
object ;
( x in [:(downarrow s),(downarrow t):] implies x in downarrow [s,t] )assume
x in [:(downarrow s),(downarrow t):]
;
x in downarrow [s,t]then consider x1,
x2 being
object such that A1:
x1 in downarrow s
and A2:
x2 in downarrow t
and A3:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider x2 =
x2 as
Element of
T by A2;
reconsider x1 =
x1 as
Element of
S by A1;
(
s >= x1 &
t >= x2 )
by A1, A2, WAYBEL_0:17;
then
[s,t] >= [x1,x2]
by YELLOW_3:11;
hence
x in downarrow [s,t]
by A3, WAYBEL_0:17;
verum
end;
let x be object ; TARSKI:def 3 ( not x in downarrow [s,t] or x in [:(downarrow s),(downarrow t):] )
assume A4:
x in downarrow [s,t]
; x in [:(downarrow s),(downarrow t):]
then reconsider x9 = x as Element of [:S,T:] ;
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then A5:
x9 = [(x9 `1),(x9 `2)]
by MCART_1:21;
A6:
[s,t] >= x9
by A4, WAYBEL_0:17;
then
t >= x9 `2
by A5, YELLOW_3:11;
then A7:
x `2 in downarrow t
by WAYBEL_0:17;
s >= x9 `1
by A5, A6, YELLOW_3:11;
then
x `1 in downarrow s
by WAYBEL_0:17;
hence
x in [:(downarrow s),(downarrow t):]
by A5, A7, ZFMISC_1:def 2; verum