let Fml be non empty set ; :: thesis: for B being Subset of Fml
for R being Rule of Fml
for a being object st B,R |- a holds
a in Fml
let B be Subset of Fml; :: thesis: for R being Rule of Fml
for a being object st B,R |- a holds
a in Fml
let R be Rule of Fml; :: thesis: for a being object st B,R |- a holds
a in Fml
let a be object ; :: thesis: ( B,R |- a implies a in Fml )
assume B,R |- a ; :: thesis: a in Fml
then consider P being Formula-sequence such that
A1: a in rng P and
A2: P is B,R -correct ;
P is Formula-sequence of Fml by A2, Lm55;
then P is FinSequence of Fml by Def5;
then rng P c= Fml by FINSEQ_1:def 4;
hence a in Fml by A1; :: thesis: verum