let Q be Quantum_Mechanics; :: thesis: for p being Element of Prop Q holds p <==> p
let p be Element of Prop Q; :: thesis: p <==> p
p |- p by Th21;
hence p <==> p by Def11; :: thesis: verum