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 ;

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

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

then consider x being object such that assume
[#] S c= L
; :: thesis: contradiction

then [#] S = L by A1;

hence contradiction by PENCIL_1:def 5; :: thesis: verum

end;then [#] S = L by A1;

hence contradiction by PENCIL_1:def 5; :: thesis: verum

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