let B be set ; :: thesis: for R being Rule
for a being object st a in B holds
B,R |- a
let R be Rule; :: thesis: for a being object st a in B holds
B,R |- a
let a be object ; :: thesis: ( a in B implies B,R |- a )
assume A1: a in B ; :: thesis: B,R |- a
then reconsider B = B as non empty set ;
reconsider t = a as Element of B by A1;
set P = <*t*>;
take <*t*> ; :: according to PROOFS_1:def 10 :: thesis: ( a in rng <*t*> & <*t*> is B,R -correct )
rng <*t*> = {t} by FINSEQ_1:38;
hence ( a in rng <*t*> & <*t*> is B,R -correct ) by TARSKI:def 1, Th40; :: thesis: verum