let S be reflexive RelStr ; :: thesis: for T being RelStr
for X being Subset of [:S,T:] holds proj2 (uparrow X) = uparrow (proj2 X)
let T be RelStr ; :: thesis: for X being Subset of [:S,T:] holds proj2 (uparrow X) = uparrow (proj2 X)
let X be Subset of [:S,T:]; :: thesis: proj2 (uparrow X) = uparrow (proj2 X)
thus proj2 (uparrow X) c= uparrow (proj2 X) by Th33; :: according to XBOOLE_0:def 10 :: thesis: uparrow (proj2 X) c= proj2 (uparrow X)
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in uparrow (proj2 X) or c in proj2 (uparrow X) )
assume A1: c in uparrow (proj2 X) ; :: thesis: c in proj2 (uparrow X)
then reconsider T9 = T as non empty RelStr ;
reconsider c9 = c as Element of T9 by A1;
consider b being Element of T9 such that
A2: b <= c9 and
A3: b in proj2 X by A1, WAYBEL_0:def 16;
consider b1 being object such that
A4: [b1,b] in X by A3, XTUPLE_0:def 13;
A5: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then reconsider S9 = S as non empty reflexive RelStr by A4, ZFMISC_1:87;
reconsider b1 = b1 as Element of S9 by A5, A4, ZFMISC_1:87;
b1 <= b1 ;
then [b1,b] <= [b1,c9] by A2, YELLOW_3:11;
then [b1,c9] in uparrow X by A4, WAYBEL_0:def 16;
hence c in proj2 (uparrow X) by XTUPLE_0:def 13; :: thesis: verum