let X be Subset of S; :: thesis: ( X is empty implies X is Open )
assume A1: X is empty ; :: thesis: X is Open
let x be Element of S; :: according to WAYBEL_6:def 1 :: thesis: ( not x in X or ex b₁ being M3( the carrier of S) st
( b₁ in X & b₁ is_way_below x ) )
assume x in X ; :: thesis: ex b₁ being M3( the carrier of S) st
( b₁ in X & b₁ is_way_below x )
hence ex b₁ being M3( the carrier of S) st
( b₁ in X & b₁ is_way_below x ) by A1; :: thesis: verum