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