let P be non empty ProofSystem ; :: thesis: ( P is paraconsistent implies P is consistent )
reconsider S = {} as empty Subset of P by XBOOLE_1:2;
assume P is paraconsistent ; :: thesis: P is consistent
then S is consistent ;
then P \/ S is consistent ;
then consider a being object such that
A1: ( a in P \/ S & not P \/ S |- a ) ;
( a in P & not P |- a ) by A1;
hence P is consistent ; :: thesis: verum