let T be non empty RelStr ; :: thesis: for p being Element of T
for k being Nat st T is filled holds
U_FT (p,k) c= U_FT (p,(k + 1))
let p be Element of T; :: thesis: for k being Nat st T is filled holds
U_FT (p,k) c= U_FT (p,(k + 1))
let k be Nat; :: thesis: ( T is filled implies U_FT (p,k) c= U_FT (p,(k + 1)) )
A1: U_FT (p,(k + 1)) = (U_FT (p,k)) ^f by FINTOPO3:48;
assume T is filled ; :: thesis: U_FT (p,k) c= U_FT (p,(k + 1))
hence U_FT (p,k) c= U_FT (p,(k + 1)) by A1, FINTOPO3:1; :: thesis: verum