let S be non empty RelStr ; :: thesis: for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (downarrow x) = downarrow (x `1)
let T be non empty reflexive RelStr ; :: thesis: for x being Element of [:S,T:] holds proj1 (downarrow x) = downarrow (x `1)
let x be Element of [:S,T:]; :: thesis: proj1 (downarrow x) = downarrow (x `1)
A1: x `2 <= x `2 ;
thus proj1 (downarrow x) c= downarrow (x `1) by Th37; :: according to XBOOLE_0:def 10 :: thesis: downarrow (x `1) c= proj1 (downarrow x)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in downarrow (x `1) or a in proj1 (downarrow x) )
assume A2: a in downarrow (x `1) ; :: thesis: a in proj1 (downarrow x)
then reconsider a9 = a as Element of S ;
a9 <= x `1 by A2, WAYBEL_0:17;
then [a9,(x `2)] <= [(x `1),(x `2)] by A1, YELLOW_3:11;
then A3: [a9,(x `2)] in downarrow [(x `1),(x `2)] by WAYBEL_0:17;
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 a in proj1 (downarrow x) by A3, XTUPLE_0:def 12; :: thesis: verum