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 A2: a in rng <*p*> ; :: thesis: a in X
a in {p} by A2, FINSEQ_1:55;
hence a in X by A1, TARSKI:def 1; :: thesis: verum

end;

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