let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for S being GRZ-formula-finset st A,R |- S holds
ex S1 being GRZ-formula-finset st
( S c= S1 & S1 is A,R -correct )
let R be GRZ-rule; :: thesis: for S being GRZ-formula-finset st A,R |- S holds
ex S1 being GRZ-formula-finset st
( S c= S1 & S1 is A,R -correct )
let S be GRZ-formula-finset; :: thesis: ( A,R |- S implies ex S1 being GRZ-formula-finset st
( S c= S1 & S1 is A,R -correct ) )
assume A1: A,R |- S ; :: thesis: ex S1 being GRZ-formula-finset st
( S c= S1 & S1 is A,R -correct )
defpred S1[ set ] means ex S1 being GRZ-formula-finset st
( $1 c= S1 & S1 is A,R -correct );
A2: S is finite ;
A10: S1[ {} ]
proof
reconsider t = the Element of A as GRZ-formula ;
consider S1 being GRZ-formula-finset such that
t in S1 and
A11: S1 is A,R -correct by Th45, Th46;
take S1 ; :: thesis: ( {} c= S1 & S1 is A,R -correct )
thus ( {} c= S1 & S1 is A,R -correct ) by A11; :: thesis: verum
end;
A20: for x, B being set st x in S & B c= S & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in S & B c= S & S1[B] implies S1[B \/ {x}] )
assume that
A21: x in S and
B c= S and
A23: S1[B] ; :: thesis: S1[B \/ {x}]
reconsider t = x as GRZ-formula by A21;
consider S1 being GRZ-formula-finset such that
A24: t in S1 and
A25: S1 is A,R -correct by A1, A21, Th45;
consider S2 being GRZ-formula-finset such that
A26: B c= S2 and
A27: S2 is A,R -correct by A23;
take S1 \/ S2 ; :: thesis: ( B \/ {x} c= S1 \/ S2 & S1 \/ S2 is A,R -correct )
{x} c= S1 by A24, TARSKI:def 1;
hence B \/ {x} c= S1 \/ S2 by A26, XBOOLE_1:13; :: thesis: S1 \/ S2 is A,R -correct
thus S1 \/ S2 is A,R -correct by A25, A27, Th43; :: thesis: verum
end;
thus S1[S] from FINSET_1:sch 2(A2, A10, A20); :: thesis: verum