set c = the Component of the Sorts of A;
take the Component of the Sorts of A ; :: thesis: the Component of the Sorts of A is Component of the Sorts of A
thus the Component of the Sorts of A is Component of the Sorts of A ; :: thesis: verum