consider x being Element of Leaves T;
reconsider x = x 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