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

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