[::] c= [#] Sorgenfrey-plane
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in or z in [#] Sorgenfrey-plane )
assume z in ; :: thesis:
then consider x, y being object such that
A1: ( x in RAT & y in RAT ) and
A2: z = [x,y] by ZFMISC_1:def 2;
( x in REAL & y in REAL ) by ;
then ( x in [#] Sorgenfrey-line & y in [#] Sorgenfrey-line ) by TOPGEN_3:def 2;
then z in by ;
hence z in [#] Sorgenfrey-plane ; :: thesis: verum
end;
then reconsider C = as Subset of Sorgenfrey-plane ;
for A being Subset of Sorgenfrey-plane st A <> {} & A is open holds
A meets C
proof
let A be Subset of Sorgenfrey-plane; :: thesis: ( A <> {} & A is open implies A meets C )
assume that
A3: A <> {} and
A4: A is open ; :: thesis: A meets C
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 ;
now :: thesis: ex e being set st
( e in B & not e = {} )
assume A7: for e being set st e in B holds
e = {} ; :: thesis: contradiction
union B c= {}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union B or z in {} )
assume z in union B ; :: thesis: z in {}
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: verum
end;
hence contradiction by A5, A3; :: thesis: verum
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 ;
consider x1 being object such that
A13: x1 in X1 by ;
consider y1 being object such that
A14: y1 in Y1 by ;
consider ax being Subset of Sorgenfrey-line such that
A15: ax in BB and
x1 in ax and
A16: ax c= X1 by ;
consider ay being Subset of Sorgenfrey-line such that
A17: ay in BB and
y1 in ay and
A18: ay c= Y1 by ;
consider px, qx being Real such that
A19: ax = [.px,qx.[ and
A20: ( px < qx & qx is rational ) by ;
consider py, qy being Real such that
A21: ay = [.py,qy.[ and
A22: ( py < qy & qy is rational ) by ;
consider rx being Rational such that
A23: ( px < rx & rx < qx ) by ;
A24: rx in ax by ;
consider ry being Rational such that
A25: ( py < ry & ry < qy ) by ;
A26: ry in ay by ;
( 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 ;
then A28: [rx,ry] in A by ;
thus A meets C by ; :: thesis: verum
end;
hence [::] is dense Subset of Sorgenfrey-plane by TOPS_1:45; :: thesis: verum