let X be Subset of CQC-WFF; :: thesis: for p being Element of CQC-WFF st p in X holds
X |- p
let p be Element of CQC-WFF ; :: thesis: ( p in X implies X |- p )
assume A1: p in X ; :: thesis: X |- p

now

let a be set ; :: thesis: ( a in rng <*p*> implies a in X )
assume a in rng <*p*> ; :: thesis: a in X
then a in {p} by FINSEQ_1:38;
hence a in X by A1, TARSKI:def 1; :: thesis: verum

end;

then A2: rng <*p*> c= X by TARSKI:def 3;
|- ((<*> CQC-WFF) ^ <*p*>) ^ <*p*> by CALCUL_2:21;
then |- <*p*> ^ <*p*> by FINSEQ_1:34;
hence X |- p by A2, HENMODEL:def 1; :: thesis: verum