let S, T be RelStr ; :: thesis: 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:]; :: thesis: ( 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 :: according to TARSKI:def 3 :: thesis: proj2 (downarrow X) c= downarrow (proj2 X)
let a be
set ;
:: thesis: ( a in proj1 (downarrow X) implies a in downarrow (proj1 X) )assume
a in proj1 (downarrow X)
;
:: thesis: a in downarrow (proj1 X)then consider b being
set such that A2:
[a,b] in downarrow 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
T' by A1, A2, ZFMISC_1:106;
reconsider a' =
a as
Element of
S' 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 15;
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 downarrow (proj1 X)
by WAYBEL_0:def 15;
:: thesis: verum
end;
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in proj2 (downarrow X) or b in downarrow (proj2 X) )
assume
b in proj2 (downarrow X)
; :: thesis: b in downarrow (proj2 X)
then consider a being set such that
A4:
[a,b] in downarrow 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 T' by A1, A4, ZFMISC_1:106;
reconsider a' = a as Element of S' by A1, A4, ZFMISC_1:106;
consider c being Element of [:S',T':] such that
A5:
( [a',b'] <= c & c in X )
by A4, WAYBEL_0:def 15;
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 downarrow (proj2 X)
by WAYBEL_0:def 15; :: thesis: verum