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