let T be non empty RelStr ; :: thesis: for A being Subset of T st T is filled holds
A c= A ^f
let A be Subset of T; :: thesis: ( T is filled implies A c= A ^f )
assume A1: T is filled ; :: thesis: A c= A ^f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A ^f )
assume A2: x in A ; :: thesis: x in A ^f
then reconsider y = x as Element of T ;
y in U_FT y by A1, FIN_TOPO:def 4;
hence x in A ^f by A2, FIN_TOPO:11; :: thesis: verum