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 M3( the carrier of S) st
( z in proj1 X & z << s ) )
assume s in proj1 X ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: z << s
thus z << s by A5, A6, Th18; :: thesis: verum

end;

let t be Element of T; :: according to WAYBEL_6:def 1 :: thesis: ( not t in proj2 X or ex b₁ being M3( the carrier of T) st
( b₁ in proj2 X & b₁ is_way_below t ) )
assume t in proj2 X ; :: thesis: ex b₁ being M3( the carrier of T) st
( b₁ in proj2 X & b₁ 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 ; :: thesis: ( 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; :: thesis: z is_way_below t
thus z is_way_below t by A9, A10, Th18; :: thesis: verum