let S be non void non degenerated TopStruct ; :: thesis: for L being Block of S holds
not for x being Point of S holds x in L
let L be Block of S; :: thesis: not for x being Point of S holds x in L
A1: L in the topology of S ;

now

assume [#] S c= L ; :: thesis: contradiction
then [#] S = L by A1, XBOOLE_0:def 10;
hence contradiction by PENCIL_1:def 5; :: thesis: verum

end;

then consider x being set such that
A2: ( x in [#] S & not x in L ) by TARSKI:def 3;
reconsider x = x as Point of S by A2;
take x ; :: thesis: not x in L
thus not x in L by A2; :: thesis: verum