let S, T be RelStr ; for X being Subset of holds
( proj1 (uparrow X) c= uparrow (proj1 X) & proj2 (uparrow X) c= uparrow (proj2 X) )
let X be Subset of ; ( proj1 (uparrow X) c= uparrow (proj1 X) & proj2 (uparrow X) c= uparrow (proj2 X) )
A1:
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
by YELLOW_3:def 2;
hereby TARSKI:def 3 proj2 (uparrow X) c= uparrow (proj2 X)
let a be
set ;
( a in proj1 (uparrow X) implies a in uparrow (proj1 X) )assume
a in proj1 (uparrow X)
;
a in uparrow (proj1 X)then consider b being
set such that A2:
[a,b] in uparrow X
by RELAT_1:def 4;
reconsider S' =
S,
T' =
T as non
empty RelStr by A1, A2, ZFMISC_1:106;
reconsider b' =
b as
Element of
by A1, A2, ZFMISC_1:106;
reconsider a' =
a as
Element of
by A1, A2, ZFMISC_1:106;
consider c being
Element of
such that A3:
(
[a',b'] >= c &
c in X )
by A2, WAYBEL_0:def 16;
c = [(c `1 ),(c `2 )]
by A1, MCART_1:23;
then
(
a' >= c `1 &
c `1 in proj1 X )
by A3, FUNCT_5:4, YELLOW_3:11;
hence
a in uparrow (proj1 X)
by WAYBEL_0:def 16;
verum
end;
let b be set ; TARSKI:def 3 ( not b in proj2 (uparrow X) or b in uparrow (proj2 X) )
assume
b in proj2 (uparrow X)
; b in uparrow (proj2 X)
then consider a being set such that
A4:
[a,b] in uparrow X
by RELAT_1:def 5;
reconsider S' = S, T' = T as non empty RelStr by A1, A4, ZFMISC_1:106;
reconsider b' = b as Element of by A1, A4, ZFMISC_1:106;
reconsider a' = a as Element of by A1, A4, ZFMISC_1:106;
consider c being Element of such that
A5:
( [a',b'] >= c & c in X )
by A4, WAYBEL_0:def 16;
c = [(c `1 ),(c `2 )]
by A1, MCART_1:23;
then
( b' >= c `2 & c `2 in proj2 X )
by A5, FUNCT_5:4, YELLOW_3:11;
hence
b in uparrow (proj2 X)
by WAYBEL_0:def 16; verum