for r being Real holds
( Vertical_Line r is closed & Horizontal_Line r is closed ) by Th6, Th9;