:: deftheorem Def2 defines Sorgenfrey-line TOPGEN_3:def 2 :
for b₁ being non empty strict TopSpace holds
( b₁ = Sorgenfrey-line iff ( the carrier of b₁ = REAL & ex B being Subset-Family of REAL st
( the topology of b₁ = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) ) );