set t = the transition of P;
take { the transition of P} ; :: thesis: for x being set st x in { the transition of P} holds
x is transition of P
thus for x being set st x in { the transition of P} holds
x is transition of P by TARSKI:def 1; :: thesis: verum