let S, T be RelStr ; for X being Subset of [:S,T:] holds
( proj1 (downarrow X) c= downarrow (proj1 X) & proj2 (downarrow X) c= downarrow (proj2 X) )
let X be Subset of [:S,T:]; ( proj1 (downarrow X) c= downarrow (proj1 X) & proj2 (downarrow X) c= downarrow (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 (downarrow X) c= downarrow (proj2 X)
let a be
object ;
( a in proj1 (downarrow X) implies a in downarrow (proj1 X) )assume
a in proj1 (downarrow X)
;
a in downarrow (proj1 X)then consider b being
object such that A2:
[a,b] in downarrow X
by XTUPLE_0:def 12;
reconsider S9 =
S,
T9 =
T as non
empty RelStr by A1, A2, ZFMISC_1:87;
reconsider b9 =
b as
Element of
T9 by A1, A2, ZFMISC_1:87;
reconsider a9 =
a as
Element of
S9 by A1, A2, ZFMISC_1:87;
consider c being
Element of
[:S9,T9:] such that A3:
(
[a9,b9] <= c &
c in X )
by A2, WAYBEL_0:def 15;
c = [(c `1),(c `2)]
by A1, MCART_1:21;
then
(
a9 <= c `1 &
c `1 in proj1 X )
by A3, XTUPLE_0:def 12, YELLOW_3:11;
hence
a in downarrow (proj1 X)
by WAYBEL_0:def 15;
verum
end;
let b be object ; TARSKI:def 3 ( not b in proj2 (downarrow X) or b in downarrow (proj2 X) )
assume
b in proj2 (downarrow X)
; b in downarrow (proj2 X)
then consider a being object such that
A4:
[a,b] in downarrow X
by XTUPLE_0:def 13;
reconsider S9 = S, T9 = T as non empty RelStr by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1, A4, ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1, A4, ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A5:
( [a9,b9] <= c & c in X )
by A4, WAYBEL_0:def 15;
c = [(c `1),(c `2)]
by A1, MCART_1:21;
then
( b9 <= c `2 & c `2 in proj2 X )
by A5, XTUPLE_0:def 13, YELLOW_3:11;
hence
b in downarrow (proj2 X)
by WAYBEL_0:def 15; verum