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

now :: thesis: for a being object st a in rng <*p*> holds
a in X

let a be object ; :: 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 ;
|- ((<*> (CQC-WFF Al)) ^ <*p*>) ^ <*p*> by CALCUL_2:21;
then |- <*p*> ^ <*p*> by FINSEQ_1:34;
hence X |- p by A2, HENMODEL:def 1; :: thesis: verum