consider k being Element of F such that
A2: a _|_ by A1, Def1;
take k ; :: thesis: for l being Element of F st a _|_ holds
k = l
let l be Element of F; :: thesis: ( a _|_ implies k = l )
assume a _|_ ; :: thesis: k = l
hence k = l by A1, A2, Th12; :: thesis: verum