let X be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( [#] L is directed implies f .: (# (Tails L)) is basis of (filter_image (f,(Tails_Filter L))) )
assume A1: [#] L is directed ; :: thesis: 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))) ; :: thesis: verum