let S, T be non empty up-complete Poset; :: thesis: for X being Subset of S
for Y being Subset of T st X is Open & Y is Open holds
[:X,Y:] is Open
let X be Subset of S; :: thesis: for Y being Subset of T st X is Open & Y is Open holds
[:X,Y:] is Open
let Y be Subset of T; :: thesis: ( X is Open & Y is Open implies [:X,Y:] is Open )
assume that
A1: for x being Element of S st x in X holds
ex y being Element of S st
( y in X & y << x ) and
A2: for x being Element of T st x in Y holds
ex y being Element of T st
( y in Y & y << x ) ; :: according to WAYBEL_6:def 1 :: thesis: [:X,Y:] is Open
let x be Element of [:S,T:]; :: according to WAYBEL_6:def 1 :: thesis: ( not x in [:X,Y:] or ex b₁ being M2(the carrier of [:S,T:]) st
( b₁ in [:X,Y:] & b₁ is_way_below x ) )
assume A3: x in [:X,Y:] ; :: thesis: ex b₁ being M2(the carrier of [:S,T:]) st
( b₁ in [:X,Y:] & b₁ is_way_below x )
then A4: x = [(x `1 ),(x `2 )] by MCART_1:23;
then x `1 in X by A3, ZFMISC_1:106;
then consider s being Element of S such that
A5: ( s in X & s << x `1 ) by A1;
x `2 in Y by A3, A4, ZFMISC_1:106;
then consider t being Element of T such that
A6: ( t in Y & t << x `2 ) by A2;
reconsider t = t as Element of T ;
take [s,t] ; :: thesis: ( [s,t] in [:X,Y:] & [s,t] is_way_below x )
thus [s,t] in [:X,Y:] by A5, A6, ZFMISC_1:106; :: thesis: [s,t] is_way_below x
thus [s,t] is_way_below x by A4, A5, A6, Th19; :: thesis: verum