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

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