let X be Subset of ; :: thesis: for a, b being Point of st X = ].a,b.[ holds
X is open
let a, b be Point of ; :: thesis: ( X = ].a,b.[ implies X is open )
assume A1: X = ].a,b.[ ; :: thesis: X is open
then reconsider X' = X as Subset of by Th44;
X' is open by A1, Th70;
hence X is open by Th59, TSEP_1:17; :: thesis: verum