let A be Subset of Sorgenfrey-plane; :: thesis:
assume that
A3: A <> {} and
A4: A is open ; :: thesis:
consider B being Subset-Family of Sorgenfrey-plane such that
A5: A = union B and
A6: for e being set st e in B holds
ex X1, Y1 being Subset of Sorgenfrey-line st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5, A4;

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in union B ; :: thesis:
then consider y being set such that
A8: ( z in y & y in B ) by TARSKI:def 4;
thus z in {} by A8, A7; :: thesis:

end;

end;

then consider e being set such that
A9: ( e in B & e <> {} ) ;
consider X1, Y1 being Subset of Sorgenfrey-line such that
A10: e = [:X1,Y1:] and
A11: ( X1 is open & Y1 is open ) by A6, A9;
A12: ( X1 <> {} & Y1 <> {} ) by ZFMISC_1:90, A9, A10;
consider x1 being object such that
A13: x1 in X1 by A12, XBOOLE_0:7;
consider y1 being object such that
A14: y1 in Y1 by A12, XBOOLE_0:7;
consider ax being Subset of Sorgenfrey-line such that
A15: ax in BB and
x1 in ax and
A16: ax c= X1 by YELLOW_9:31, A11, A13, Lm8;
consider ay being Subset of Sorgenfrey-line such that
A17: ay in BB and
y1 in ay and
A18: ay c= Y1 by YELLOW_9:31, A11, A14, Lm8;
consider px, qx being Real such that
A19: ax = [.px,qx.[ and
A20: ( px < qx & qx is rational ) by A15, Lm7;
consider py, qy being Real such that
A21: ay = [.py,qy.[ and
A22: ( py < qy & qy is rational ) by A17, Lm7;
consider rx being Rational such that
A23: ( px < rx & rx < qx ) by RAT_1:7, A20;
A24: rx in ax by A23, XXREAL_1:3, A19;
consider ry being Rational such that
A25: ( py < ry & ry < qy ) by RAT_1:7, A22;
A26: ry in ay by A25, XXREAL_1:3, A21;
( rx in RAT & ry in RAT ) by RAT_1:def 2;
then A27: [rx,ry] in C by ZFMISC_1:def 2;
[rx,ry] in [:X1,Y1:] by A24, A26, A16, A18, ZFMISC_1:def 2;
then A28: [rx,ry] in A by A5, A9, A10, TARSKI:def 4;
thus A meets C by A27, A28, XBOOLE_0:3; :: thesis:

end;