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