let S be non empty reflexive RelStr ; :: thesis: for T being non empty RelStr
for x being Element of [:S,T:] holds proj2 (uparrow x) = uparrow (x `2)
let T be non empty RelStr ; :: thesis: for x being Element of [:S,T:] holds proj2 (uparrow x) = uparrow (x `2)
let x be Element of [:S,T:]; :: thesis: proj2 (uparrow x) = uparrow (x `2)
A1: x `1 <= x `1 ;
thus proj2 (uparrow x) c= uparrow (x `2) by Th41; :: according to XBOOLE_0:def 10 :: thesis: uparrow (x `2) c= proj2 (uparrow x)
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in uparrow (x `2) or b in proj2 (uparrow x) )
assume A2: b in uparrow (x `2) ; :: thesis: b in proj2 (uparrow x)
then reconsider b9 = b as Element of T ;
b9 >= x `2 by A2, WAYBEL_0:18;
then [(x `1),b9] >= [(x `1),(x `2)] by A1, YELLOW_3:11;
then A3: [(x `1),b9] in uparrow [(x `1),(x `2)] by WAYBEL_0:18;
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then x = [(x `1),(x `2)] by MCART_1:21;
hence b in proj2 (uparrow x) by A3, XTUPLE_0:def 13; :: thesis: verum