[mizar] referring to unlabeled theorems

[Jesse Alama <alama@stanford.edu>]

I'm trying to use FVSUM_1:22 in a proof I'm working on, but I get
error *192 ("Inaccessible theorem") when doing so.  The problem seems
to be that the twenty-second theorem of FVSUM_1 is not labeled as
such, even though the semantic presentation of FVSUM_1 does assign a
label to this theorem.  How can I refer to this theorem?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*102: Unknown predicate (http://www.mizar.org)