set a = the object ;
reconsider X = { the object } as non empty set ;
reconsider B = {} as Subset of X by XBOOLE_1:2;
reconsider R = {} as Rule ;
( dom R c= Fin X & rng R c= X ) ;
then reconsider R = R as Rule of X by Def2;
reconsider P = ProofSystem(# X,B,R #) as non empty ProofSystem ;
take P ; :: thesis: ( P is consistent & P is strict )
thus P is consistent :: thesis: P is strict

proof

take the object ; :: according to PROOFS_1:def 19 :: thesis: ( the object in P & not P |- the object )
thus the object in P by TARSKI:def 1; :: thesis: not P |- the object
( not the object in B & ( for S being Formula-finset holds
( not [S, the object ] in R or ex b being object st
( b in S & not B,R |- b ) ) ) ) ;
hence not P |- the object by Th51; :: thesis: verum

end;

thus P is strict ; :: thesis: verum