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