:: deftheorem defines Sorgenfrey-plane TOPGEN_6:def 1 :
Sorgenfrey-plane = [:Sorgenfrey-line,Sorgenfrey-line:];