let B be set ; :: thesis: for R being Rule
for t being object holds
( B,R |- t iff ex S being Formula-finset st
( t in S & S is B,R -derivable ) )
let R be Rule; :: thesis: for t being object holds
( B,R |- t iff ex S being Formula-finset st
( t in S & S is B,R -derivable ) )
let t be object ; :: thesis: ( B,R |- t iff ex S being Formula-finset st
( t in S & S is B,R -derivable ) )
thus ( B,R |- t implies ex S being Formula-finset st
( t in S & S is B,R -derivable ) ) :: thesis: ( ex S being Formula-finset st
( t in S & S is B,R -derivable ) implies B,R |- t )

proof

assume B,R |- t ; :: thesis: ex S being Formula-finset st
( t in S & S is B,R -derivable )
then consider P being Formula-sequence such that
A1: t in rng P and
A2: P is B,R -correct ;
take S = rng P; :: thesis: ( t in S & S is B,R -derivable )
thus t in S by A1; :: thesis: S is B,R -derivable
thus S is B,R -derivable by A2; :: thesis: verum

end;

given S being Formula-finset such that A10: t in S and
A11: S is B,R -derivable ; :: thesis: B,R |- t
consider P being Formula-sequence such that
A12: S = rng P and
A13: P is B,R -correct by A11;
thus B,R |- t by A10, A12, A13; :: thesis: verum