reconsider P = <*> Fml as Formula-sequence of Fml by Def5;
take P ; :: thesis: P is B,R -correct
thus P is B,R -correct ; :: thesis: verum