let S, T be RelStr ; :: thesis: for X being Subset of [:S,T:] holds downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
let X be Subset of [:S,T:]; :: thesis: downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow X or x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):] )
assume A2: x in downarrow X ; :: thesis: x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
then consider a, b being set such that
A3: ( a in the carrier of S & b in the carrier of T ) and
x = [a,b] by A1, ZFMISC_1:def 2;
reconsider S' = S, T' = T as non empty RelStr by A3;
reconsider x' = x as Element of [:S',T':] by A2;
consider y being Element of [:S',T':] such that
A4: ( y >= x' & y in X ) by A2, WAYBEL_0:def 15;
A5: ( y `1 >= x' `1 & y `2 >= x' `2 ) by A4, YELLOW_3:12;
y = [(y `1 ),(y `2 )] by A1, MCART_1:23;
then ( y `1 in proj1 X & y `2 in proj2 X ) by A4, FUNCT_5:4;
then A6: ( x `1 in downarrow (proj1 X) & x `2 in downarrow (proj2 X) ) by A5, WAYBEL_0:def 15;
x' = [(x' `1 ),(x' `2 )] by A1, MCART_1:23;
hence x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):] by A6, MCART_1:11; :: thesis: verum