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 & SCM-OK . t = INT ) by Th8, Th9;
hence a <> t by Th6; :: thesis: verum