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

proof

assume A2: for a being set holds P₁[a] ; :: thesis: for a being set holds P₂[a]

now

let a be set ; :: thesis: P₂[a]
( P₁[a] iff P₂[a] ) by A1;
hence P₂[a] by A2; :: thesis: verum

end;

hence for a being set holds P₂[a] ; :: thesis: verum

end;

assume A3: for a being set holds P₂[a] ; :: thesis: for a being set holds P₁[a]

now

let a be set ; :: thesis: P₁[a]
( P₁[a] iff P₂[a] ) by A1;
hence P₁[a] by A3; :: thesis: verum

end;

hence for a being set holds P₁[a] ; :: thesis: verum