let a be Element of NAT ; :: thesis: for t being Element of SCM-Data-Loc holds a <> t
let t be Element of SCM-Data-Loc ; :: thesis: a <> t
SCM-OK . a = SCM-Instr by Th9;
hence a <> t by Th6, Th8; :: thesis: verum