let X be non empty set ; for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X st [#] L is directed holds
f .: (# (Tails L)) is basis of (filter_image (f,(Tails_Filter L)))
let L be non empty reflexive transitive RelStr ; for f being Function of ([#] L),X st [#] L is directed holds
f .: (# (Tails L)) is basis of (filter_image (f,(Tails_Filter L)))
let f be Function of ([#] L),X; ( [#] L is directed implies f .: (# (Tails L)) is basis of (filter_image (f,(Tails_Filter L))) )
assume A1:
[#] L is directed
; f .: (# (Tails L)) is basis of (filter_image (f,(Tails_Filter L)))
reconsider SL = Tails L as basis of (Tails_Filter L) by A1, Th15;
f .: (# SL) is basis of (filter_image (f,(Tails_Filter L)))
by Th13bThmBA2;
hence
f .: (# (Tails L)) is basis of (filter_image (f,(Tails_Filter L)))
; verum