reconsider b9 = b as Element of ObjectKind lb by Th1;
reconsider a9 = a as Element of ObjectKind la by Th1;
la,lb --> a9,b9 is FinPartState of (SCM R) ;
hence la,lb --> a,b is FinPartState of (SCM R) ; :: thesis: verum