let S be reflexive RelStr ; :: thesis: for T being RelStr
for X being Subset of [:S,T:] holds proj2 (downarrow X) = downarrow (proj2 X)
let T be RelStr ; :: thesis: for X being Subset of [:S,T:] holds proj2 (downarrow X) = downarrow (proj2 X)
let X be Subset of [:S,T:]; :: thesis: proj2 (downarrow X) = downarrow (proj2 X)
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
thus proj2 (downarrow X) c= downarrow (proj2 X) by Th28; :: according to XBOOLE_0:def 10 :: thesis: downarrow (proj2 X) c= proj2 (downarrow X)
let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in downarrow (proj2 X) or c in proj2 (downarrow X) )
assume A2: c in downarrow (proj2 X) ; :: thesis: c in proj2 (downarrow X)
then reconsider T' = T as non empty RelStr ;
reconsider c' = c as Element of T' by A2;
consider b being Element of T' such that
A3: ( b >= c' & b in proj2 X ) by A2, WAYBEL_0:def 15;
consider b1 being set such that
A4: [b1,b] in X by A3, RELAT_1:def 5;
b1 in the carrier of S by A1, A4, ZFMISC_1:106;
then reconsider S' = S as non empty reflexive RelStr ;
reconsider b1 = b1 as Element of S' by A1, A4, ZFMISC_1:106;
b1 <= b1 ;
then [b1,b] >= [b1,c'] by A3, YELLOW_3:11;
then [b1,c'] in downarrow X by A4, WAYBEL_0:def 15;
hence c in proj2 (downarrow X) by RELAT_1:def 5; :: thesis: verum