let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for X being Subset of [:S,T:] st X is Open holds
( proj1 X is Open & proj2 X is Open )
let X be Subset of [:S,T:]; :: thesis: ( X is Open implies ( proj1 X is Open & proj2 X is Open ) )
assume A1:
for x being Element of [:S,T:] st x in X holds
ex y being Element of [:S,T:] st
( y in X & y << x )
; :: according to WAYBEL_6:def 1 :: thesis: ( proj1 X is Open & proj2 X is Open )
A2:
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
by YELLOW_3:def 2;
hereby :: according to WAYBEL_6:def 1 :: thesis: proj2 X is Open
let s be
Element of
S;
:: thesis: ( s in proj1 X implies ex z being M2(the carrier of S) st
( z in proj1 X & z << s ) )assume
s in proj1 X
;
:: thesis: ex z being M2(the carrier of S) st
( z in proj1 X & z << s )then consider t being
set such that A3:
[s,t] in X
by RELAT_1:def 4;
reconsider t =
t as
Element of
T by A2, A3, ZFMISC_1:106;
consider y being
Element of
[:S,T:] such that A4:
(
y in X &
y << [s,t] )
by A1, A3;
take z =
y `1 ;
:: thesis: ( z in proj1 X & z << s )A5:
y = [(y `1 ),(y `2 )]
by A2, MCART_1:23;
hence
z in proj1 X
by A4, RELAT_1:def 4;
:: thesis: z << sthus
z << s
by A4, A5, Th18;
:: thesis: verum
end;
let t be Element of T; :: according to WAYBEL_6:def 1 :: thesis: ( not t in proj2 X or ex b1 being M2(the carrier of T) st
( b1 in proj2 X & b1 is_way_below t ) )
assume
t in proj2 X
; :: thesis: ex b1 being M2(the carrier of T) st
( b1 in proj2 X & b1 is_way_below t )
then consider s being set such that
A6:
[s,t] in X
by RELAT_1:def 5;
reconsider s = s as Element of S by A2, A6, ZFMISC_1:106;
consider y being Element of [:S,T:] such that
A7:
( y in X & y << [s,t] )
by A1, A6;
take z = y `2 ; :: thesis: ( z in proj2 X & z is_way_below t )
A8:
y = [(y `1 ),(y `2 )]
by A2, MCART_1:23;
hence
z in proj2 X
by A7, RELAT_1:def 5; :: thesis: z is_way_below t
thus
z is_way_below t
by A7, A8, Th18; :: thesis: verum