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 object such that
A1: ( y `1 c= X & y `2 = x & {y} is D -derivable ) ;
reconsider E = {} as Subset of (S -sequents) by XBOOLE_1:2;
{y} is {} ,D -derivable by A1;
then consider mm being Element of NAT such that
A2: y is mm,E,D -derivable by Lm8;
reconsider yy = y as Element of S -sequents by Def2, A2;
yy `2 is wff string of S by Lm24;
hence x is wff string of S by A1; :: thesis: verum