let T be non empty RelStr ; :: thesis: for p being Element of T
for k being Element of 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 Element of NAT st T is filled holds
U_FT p,k c= U_FT p,(k + 1)
let k be Element of 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