let S be non empty RelStr ; :: thesis: for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1 )
let T be non empty reflexive RelStr ; :: thesis: for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1 )
let x be Element of [:S,T:]; :: thesis: proj1 (uparrow x) = uparrow (x `1 )
A1: x `2 <= x `2 ;
thus proj1 (uparrow x) c= uparrow (x `1 ) by Th41; :: according to XBOOLE_0:def 10 :: thesis: uparrow (x `1 ) c= proj1 (uparrow x)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in uparrow (x `1 ) or a in proj1 (uparrow x) )
assume A2: a in uparrow (x `1 ) ; :: thesis: a in proj1 (uparrow x)
then reconsider a' = a as Element of S ;
a' >= x `1 by A2, WAYBEL_0:18;
then [a',(x `2 )] >= [(x `1 ),(x `2 )] by A1, YELLOW_3:11;
then A3: [a',(x `2 )] 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:23;
hence a in proj1 (uparrow x) by A3, RELAT_1:def 4; :: thesis: verum