let MS be OrtAfPl; :: thesis: ( MS is translation iff MS is satisfying_des )
set AS = Af MS;

A1: now :: thesis: ( MS is satisfying_des implies MS is translation )

assume MS is satisfying_des ; :: thesis: MS is translation
then Af MS is translational by Lm3;
hence MS is translation by Def6; :: thesis: verum

end;

now :: thesis: ( MS is translation implies MS is satisfying_des )

assume MS is translation ; :: thesis: MS is satisfying_des
then Af MS is translational by Def6;
hence MS is satisfying_des by Lm3; :: thesis: verum

end;

hence ( MS is translation iff MS is satisfying_des ) by A1; :: thesis: verum