let S, T be non empty reflexive antisymmetric up-complete RelStr ; 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:]; ( 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 )
; WAYBEL_6:def 1 ( 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 WAYBEL_6:def 1 proj2 X is Open
let s be
Element of
S;
( s in proj1 X implies ex z being M3( the carrier of S) st
( z in proj1 X & z << s ) )assume
s in proj1 X
;
ex z being M3( the carrier of S) st
( z in proj1 X & z << s )then consider t being
object such that A3:
[s,t] in X
by XTUPLE_0:def 12;
reconsider t =
t as
Element of
T by A2, A3, ZFMISC_1:87;
consider y being
Element of
[:S,T:] such that A4:
y in X
and A5:
y << [s,t]
by A1, A3;
take z =
y `1 ;
( z in proj1 X & z << s )A6:
y = [(y `1),(y `2)]
by A2, MCART_1:21;
hence
z in proj1 X
by A4, XTUPLE_0:def 12;
z << sthus
z << s
by A5, A6, Th18;
verum
end;
let t be Element of T; WAYBEL_6:def 1 ( not t in proj2 X or ex b1 being M3( the carrier of T) st
( b1 in proj2 X & b1 is_way_below t ) )
assume
t in proj2 X
; ex b1 being M3( the carrier of T) st
( b1 in proj2 X & b1 is_way_below t )
then consider s being object such that
A7:
[s,t] in X
by XTUPLE_0:def 13;
reconsider s = s as Element of S by A2, A7, ZFMISC_1:87;
consider y being Element of [:S,T:] such that
A8:
y in X
and
A9:
y << [s,t]
by A1, A7;
take z = y `2 ; ( z in proj2 X & z is_way_below t )
A10:
y = [(y `1),(y `2)]
by A2, MCART_1:21;
hence
z in proj2 X
by A8, XTUPLE_0:def 13; z is_way_below t
thus
z is_way_below t
by A9, A10, Th18; verum