let S, T be non empty reflexive antisymmetric up-complete RelStr ; for x being Element of holds
( proj1 (compactbelow x) c= compactbelow (x `1 ) & proj2 (compactbelow x) c= compactbelow (x `2 ) )
let x be Element of ; ( proj1 (compactbelow x) c= compactbelow (x `1 ) & proj2 (compactbelow x) c= compactbelow (x `2 ) )
A1:
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
by YELLOW_3:def 2;
then A2:
x = [(x `1 ),(x `2 )]
by MCART_1:23;
hereby TARSKI:def 3 proj2 (compactbelow x) c= compactbelow (x `2 )
let a be
set ;
( a in proj1 (compactbelow x) implies a in compactbelow (x `1 ) )assume
a in proj1 (compactbelow x)
;
a in compactbelow (x `1 )then consider b being
set such that A3:
[a,b] in compactbelow x
by RELAT_1:def 4;
reconsider b =
b as
Element of
by A1, A3, ZFMISC_1:106;
reconsider a' =
a as
Element of
by A1, A3, ZFMISC_1:106;
(
[a',b] `1 = a' &
[a',b] is
compact )
by A3, MCART_1:7, WAYBEL_8:4;
then A4:
a' is
compact
by Th22;
[a',b] <= x
by A3, WAYBEL_8:4;
then
a' <= x `1
by A2, YELLOW_3:11;
hence
a in compactbelow (x `1 )
by A4;
verum
end;
let b be set ; TARSKI:def 3 ( not b in proj2 (compactbelow x) or b in compactbelow (x `2 ) )
assume
b in proj2 (compactbelow x)
; b in compactbelow (x `2 )
then consider a being set such that
A5:
[a,b] in compactbelow x
by RELAT_1:def 5;
reconsider a = a as Element of by A1, A5, ZFMISC_1:106;
reconsider b' = b as Element of by A1, A5, ZFMISC_1:106;
( [a,b'] `2 = b' & [a,b'] is compact )
by A5, MCART_1:7, WAYBEL_8:4;
then A6:
b' is compact
by Th22;
[a,b'] <= x
by A5, WAYBEL_8:4;
then
b' <= x `2
by A2, YELLOW_3:11;
hence
b in compactbelow (x `2 )
by A6; verum