let x, X be set ; :: thesis: for S being Language
for D being RuleSet of S st x is X,D -provable holds
x is wff string of S
let S be Language; :: thesis: for D being RuleSet of S st x is X,D -provable holds
x is wff string of S
let D be RuleSet of S; :: thesis: ( x is X,D -provable implies x is wff string of S )
set Q = S -sequents ;
assume x is X,D -provable ; :: thesis: x is wff string of S
then consider y being set such that
B1: ( y `1 c= X & y `2 = x & {y} is D -derivable ) by DefProvable2;
reconsider E = {} as Subset of (S -sequents) by XBOOLE_1:2;
{y} is {} ,D -derivable by B1;
then consider mm being Element of NAT such that
B2: y is mm,E,D -derivable by Lm3;
reconsider yy = y as Element of S -sequents by DefSeqtLike, B2;
yy `2 is wff string of S by Lm32;
hence x is wff string of S by B1; :: thesis: verum