let A be non empty set ; :: thesis: for p being Element of CQC-WFF
for J being interpretation of A holds Valid (p '&' p),J = Valid p,J
let p be Element of CQC-WFF ; :: thesis: for J being interpretation of A holds Valid (p '&' p),J = Valid p,J
let J be interpretation of A; :: thesis: Valid (p '&' p),J = Valid p,J

now

let v be Element of Valuations_in A; :: thesis: (Valid (p '&' p),J) . v = (Valid p,J) . v
thus (Valid (p '&' p),J) . v = ((Valid p,J) . v) '&' ((Valid p,J) . v) by Th22
.= (Valid p,J) . v ; :: thesis: verum

end;

hence Valid (p '&' p),J = Valid p,J by FUNCT_2:113; :: thesis: verum