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 :: thesis: not [#] S c= L

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

end;

then consider x being object such that
A2: x in [#] S and
A3: not x in L ;
reconsider x = x as Point of S by A2;
take x ; :: thesis: not x in L
thus not x in L by A3; :: thesis: verum