let Fml be non empty set ; :: thesis: for B being Subset of Fml
for R being Rule of Fml
for P being b₁,b₂ -correct Formula-sequence holds P is Formula-sequence of Fml
let B be Subset of Fml; :: thesis: for R being Rule of Fml
for P being B,b₁ -correct Formula-sequence holds P is Formula-sequence of Fml
let R be Rule of Fml; :: thesis: for P being B,R -correct Formula-sequence holds P is Formula-sequence of Fml
let P be B,R -correct Formula-sequence; :: thesis: P is Formula-sequence of Fml
set X = B \/ (rng R);
rng R c= Fml by Def2;
then A1: B \/ (rng R) c= Fml by XBOOLE_1:8;
rng P c= Fml

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng P or t in Fml )
assume t in rng P ; :: thesis: t in Fml
then B,R |- t ;
hence t in Fml by A1, Lm54; :: thesis: verum

end;

then P is FinSequence of Fml by FINSEQ_1:def 4;
hence P is Formula-sequence of Fml by Def5; :: thesis: verum