let MS be OrtAfPl; :: thesis: ( MS is Desarguesian iff MS is satisfying_DES )
set AS = Af MS;

A1: now :: thesis: ( MS is satisfying_DES implies MS is Desarguesian )

assume MS is satisfying_DES ; :: thesis: MS is Desarguesian
then Af MS is Desarguesian by Lm2;
hence MS is Desarguesian by Def3; :: thesis: verum

end;

now :: thesis: ( MS is Desarguesian implies MS is satisfying_DES )

assume MS is Desarguesian ; :: thesis: MS is satisfying_DES
then Af MS is Desarguesian by Def3;
hence MS is satisfying_DES by Lm2; :: thesis: verum

end;

hence ( MS is Desarguesian iff MS is satisfying_DES ) by A1; :: thesis: verum