let S, T be RelStr ; for X being Subset of [:S,T:] holds downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
let X be Subset of [:S,T:]; downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
let x be object ; TARSKI:def 3 ( not x in downarrow X or x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):] )
assume A1:
x in downarrow X
; x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
A2:
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 A1, ZFMISC_1:def 2;
then reconsider S9 = S, T9 = T as non empty RelStr ;
reconsider x9 = x as Element of [:S9,T9:] by A1;
consider y being Element of [:S9,T9:] such that
A3:
y >= x9
and
A4:
y in X
by A1, WAYBEL_0:def 15;
A5:
y `1 >= x9 `1
by A3, YELLOW_3:12;
A6:
y = [(y `1),(y `2)]
by A2, MCART_1:21;
then
y `1 in proj1 X
by A4, XTUPLE_0:def 12;
then A7:
x `1 in downarrow (proj1 X)
by A5, WAYBEL_0:def 15;
A8:
y `2 >= x9 `2
by A3, YELLOW_3:12;
y `2 in proj2 X
by A4, A6, XTUPLE_0:def 13;
then A9:
x `2 in downarrow (proj2 X)
by A8, WAYBEL_0:def 15;
x9 = [(x9 `1),(x9 `2)]
by A2, MCART_1:21;
hence
x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
by A7, A9, ZFMISC_1:def 2; verum