let R be non empty right_complementable add-associative right_zeroed well-unital distributive left_zeroed Euclidian doubleLoopStr ; :: thesis: R is PID
let I be Ideal of R; :: according to IDEAL_1:def 29 :: thesis: I is principal

per cases ( I = {(0. R)} or I <> {(0. R)} ) ;

suppose A1: I = {(0. R)} ; :: thesis: I is principal

set e = 0. R;
take 0. R ; :: according to IDEAL_1:def 28 :: thesis: I = {(0. R)} -Ideal
thus I = {(0. R)} -Ideal by A1, Th44; :: thesis: verum

end;

suppose I <> {(0. R)} ; :: thesis: I is principal

then consider x being Element of R such that
A2: ( x <> 0. R & x in I ) by Th96;
set I' = { y where y is Element of I : y <> 0. R } ;
A3: x in { y where y is Element of I : y <> 0. R } by A2;
{ y where y is Element of I : y <> 0. R } c= the carrier of R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of I : y <> 0. R } or x in the carrier of R )
assume x in { y where y is Element of I : y <> 0. R } ; :: thesis: x in the carrier of R
then consider y being Element of I such that
A4: ( x = y & y <> 0. R ) ;
thus x in the carrier of R by A4; :: thesis: verum

end;

then reconsider I' = { y where y is Element of I : y <> 0. R } as non empty Subset of R by A3;
consider f being Function of the carrier of R,NAT such that
A5: for a, b being Element of R st b <> 0. R holds
ex q, r being Element of R st
( a = (q * b) + r & ( r = 0. R or f . r < f . b ) ) by INT_3:def 9;
set K = { (f . i) where i is Element of I' : verum } ;
consider i being Element of I';
A6: f . i in { (f . i) where i is Element of I' : verum } ;
{ (f . i) where i is Element of I' : verum } c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . i) where i is Element of I' : verum } or x in NAT )
assume x in { (f . i) where i is Element of I' : verum } ; :: thesis: x in NAT
then consider e being Element of I' such that
A7: f . e = x ;
thus x in NAT by A7; :: thesis: verum

end;

then reconsider K = { (f . i) where i is Element of I' : verum } as non empty Subset of NAT by A6;
set k = min K;
min K in K by XXREAL_2:def 7;
then consider e being Element of I' such that
A8: f . e = min K ;
e in I' ;
then consider e' being Element of I such that
A9: ( e' = e & e' <> 0. R ) ;
reconsider e = e as Element of R ;
take e ; :: according to IDEAL_1:def 28 :: thesis: I = {e} -Ideal

now

let x be set ; :: thesis: ( ( x in I implies x in {e} -Ideal ) & ( x in {e} -Ideal implies x in I ) )

hereby :: thesis: ( x in {e} -Ideal implies x in I )

assume A10: x in I ; :: thesis: x in {e} -Ideal
then reconsider x' = x as Element of R ;
consider q, r being Element of R such that
A11: x' = (q * e) + r and
A12: ( r = 0. R or f . r < min K ) by A5, A8, A9;

now

A13: (- (q * e)) + x' = ((- (q * e)) + (q * e)) + r by A11, RLVECT_1:def 6
.= (0. R) + r by RLVECT_1:16
.= r by ALGSTR_1:def 5 ;
q * e in I by A9, Def2;
then - (q * e) in I by Th13;
then A14: r in I by A10, A13, Def1;
assume A15: r <> 0. R ; :: thesis: contradiction
then r in I' by A14;
then f . r in K ;
hence contradiction by A12, A15, XXREAL_2:def 7; :: thesis: verum

end;

then A16: x' = q * e by A11, RLVECT_1:def 7;
A17: e in {e} by TARSKI:def 1;
{e} c= {e} -Ideal by Def15;
hence x in {e} -Ideal by A16, A17, Def2; :: thesis: verum

end;

assume A18: x in {e} -Ideal ; :: thesis: x in I
{e} c= I by A9, ZFMISC_1:37;
then {e} -Ideal c= I by Def15;
hence x in I by A18; :: thesis: verum

end;

hence I = {e} -Ideal by TARSKI:2; :: thesis: verum

end;

end;