set x = the Element of Leaves T;
reconsider x = the Element of Leaves T as Element of T by A1, TARSKI:def 3;
take x ; :: thesis: x in Leaves T
thus x in Leaves T by A1; :: thesis: verum