thus ( ( for a being set holds P₁[a] ) implies for a being set holds P₂[a] ) by A1; :: thesis: verum