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