let X be non empty set ; :: thesis: for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X
for B being filter_base of X st [#] L is directed holds
( B is_coarser_than f .: (# (Tails L)) iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
let L be non empty reflexive transitive RelStr ; :: thesis: for f being Function of ([#] L),X
for B being filter_base of X st [#] L is directed holds
( B is_coarser_than f .: (# (Tails L)) iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
let f be Function of ([#] L),X; :: thesis: for B being filter_base of X st [#] L is directed holds
( B is_coarser_than f .: (# (Tails L)) iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
let B be filter_base of X; :: thesis: ( [#] L is directed implies ( B is_coarser_than f .: (# (Tails L)) iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b ) )
assume A1: [#] L is directed ; :: thesis: ( B is_coarser_than f .: (# (Tails L)) iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
hereby :: thesis: ( ( for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b ) implies B is_coarser_than f .: (# (Tails L)) )
assume A2: B is_coarser_than f .: (# (Tails L)) ; :: thesis: for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b
hereby :: thesis: verum
let b be Element of B; :: thesis: ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b
consider x0 being set such that
A3: x0 in f .: (# (Tails L)) and
A4: x0 c= b by A2;
reconsider x1 = x0 as Subset of X by A4, XBOOLE_1:1;
consider j0 being Element of L such that
A5: for i being Element of L st i >= j0 holds
f . i in x1 by A1, A3, Th17;
for i being Element of L st i >= j0 holds
f . i in b by A4, A5;
hence ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b ; :: thesis: verum
end;
end;
assume A6: for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b ; :: thesis: B is_coarser_than f .: (# (Tails L))
now :: thesis: for Y being set st Y in B holds
ex X being set st
( X in f .: (# (Tails L)) & X c= Y )
let Y be set ; :: thesis: ( Y in B implies ex X being set st
( X in f .: (# (Tails L)) & X c= Y ) )
assume A7: Y in B ; :: thesis: ex X being set st
( X in f .: (# (Tails L)) & X c= Y )
then consider i0 being Element of L such that
A8: for j being Element of L st i0 <= j holds
f . j in Y by A6;
reconsider b = Y as Subset of X by A7;
consider b0 being Element of Tails L such that
A9: f .: b0 c= b by A1, A8, Th18;
f .: b0 in f .: (# (Tails L)) by FUNCT_2:def 10;
hence ex X being set st
( X in f .: (# (Tails L)) & X c= Y ) by A9; :: thesis: verum
end;
hence B is_coarser_than f .: (# (Tails L)) ; :: thesis: verum