let T be non empty TopStruct ; :: thesis: for A being Subset of T
for p being Point of T st ( for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q ) holds
ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q
let A be Subset of T; :: thesis: for p being Point of T st ( for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q ) holds
ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q
let p be Point of T; :: thesis: ( ( for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q ) implies ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q )
assume that
A1: for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q and
A2: for K being Basis of ex Q being Subset of T st
( Q in K & A misses Q ) ; :: thesis: contradiction
set K = the Basis of ;
ex Q being Subset of T st
( Q in the Basis of & A misses Q ) by A2;
hence contradiction by A1; :: thesis: verum