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,0) c= U_FT (p,k)

let p be Element of T; :: thesis: for k being Nat st T is filled holds

U_FT (p,0) c= U_FT (p,k)

let k be Nat; :: thesis: ( T is filled implies U_FT (p,0) c= U_FT (p,k) )

defpred S_{1}[ Nat] means U_FT (p,0) c= U_FT (p,$1);

assume A1: T is filled ; :: thesis: U_FT (p,0) c= U_FT (p,k)

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A4, A2);

hence U_FT (p,0) c= U_FT (p,k) ; :: thesis: verum

for k being Nat st T is filled holds

U_FT (p,0) c= U_FT (p,k)

let p be Element of T; :: thesis: for k being Nat st T is filled holds

U_FT (p,0) c= U_FT (p,k)

let k be Nat; :: thesis: ( T is filled implies U_FT (p,0) c= U_FT (p,k) )

defpred S

assume A1: T is filled ; :: thesis: U_FT (p,0) c= U_FT (p,k)

A2: for k being Nat st S

S

proof

A4:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

U_FT (p,k) c= U_FT (p,(k + 1)) by A1, Th7;

hence S_{1}[k + 1]
by A3, XBOOLE_1:1; :: thesis: verum

end;assume A3: S

U_FT (p,k) c= U_FT (p,(k + 1)) by A1, Th7;

hence S

for i being Nat holds S

hence U_FT (p,0) c= U_FT (p,k) ; :: thesis: verum