let S, T be non empty RelStr ; for x being Element of [:S,T:] holds
( proj1 (uparrow x) c= uparrow (x `1) & proj2 (uparrow x) c= uparrow (x `2) )
let x be Element of [:S,T:]; ( proj1 (uparrow x) c= uparrow (x `1) & proj2 (uparrow x) c= uparrow (x `2) )
A1:
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then A2:
x = [(x `1),(x `2)]
by MCART_1:21;
let b be object ; TARSKI:def 3 ( not b in proj2 (uparrow x) or b in uparrow (x `2) )
assume
b in proj2 (uparrow x)
; b in uparrow (x `2)
then consider a being object such that
A4:
[a,b] in uparrow x
by XTUPLE_0:def 13;
reconsider a = a as Element of S by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T by A1, A4, ZFMISC_1:87;
[a,b9] >= x
by A4, WAYBEL_0:18;
then
b9 >= x `2
by A2, YELLOW_3:11;
hence
b in uparrow (x `2)
by WAYBEL_0:18; verum