let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of N
for p being PartState of S
for k being Element of NAT holds DataPart p c= IncIC (p,k)
let S be non empty IC-Ins-separated Mem-Struct of N; :: thesis: for p being PartState of S
for k being Element of NAT holds DataPart p c= IncIC (p,k)
let p be PartState of S; :: thesis: for k being Element of NAT holds DataPart p c= IncIC (p,k)
let k be Element of NAT ; :: thesis: DataPart p c= IncIC (p,k)
DataPart (IncIC (p,k)) = DataPart p by Th48;
hence DataPart p c= IncIC (p,k) by RELAT_1:59; :: thesis: verum