let X be non empty set ; :: thesis: for F being Filter of X
for B being basis of F
for L being Subset of (BoolePoset X) st L = # B holds
F = uparrow L
let F be Filter of X; :: thesis: for B being basis of F
for L being Subset of (BoolePoset X) st L = # B holds
F = uparrow L
let B be basis of F; :: thesis: for L being Subset of (BoolePoset X) st L = # B holds
F = uparrow L
let L be Subset of (BoolePoset X); :: thesis: ( L = # B implies F = uparrow L )
assume A1: L = # B ; :: thesis: F = uparrow L
F = <.(# B).] by Th06;
hence F = uparrow L by Th04, A1; :: thesis: verum