let L be non empty reflexive transitive RelStr ; :: thesis: for I being Ideal of L holds
( I is principal iff ex x being Element of L st I = downarrow x )
let I be Ideal of L; :: thesis: ( I is principal iff ex x being Element of L st I = downarrow x )
thus ( I is principal implies ex x being Element of L st I = downarrow x ) :: thesis: ( ex x being Element of L st I = downarrow x implies I is principal )

proof

given x being Element of L such that A1: ( x in I & x is_>=_than I ) ; :: according to WAYBEL_0:def 21 :: thesis: ex x being Element of L st I = downarrow x
take x ; :: thesis: I = downarrow x
thus I c= downarrow x :: according to XBOOLE_0:def 10 :: thesis: downarrow x c= I

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in I or y in downarrow x )
assume A2: y in I ; :: thesis: y in downarrow x
then reconsider y = y as Element of L ;
x >= y by A1, A2, LATTICE3:def 9;
hence y in downarrow x by Th17; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in downarrow x or z in I )
assume A3: z in downarrow x ; :: thesis: z in I
then reconsider z = z as Element of L ;
z <= x by A3, Th17;
hence z in I by A1, Def19; :: thesis: verum

end;

given x being Element of L such that A4: I = downarrow x ; :: thesis: I is principal
take x ; :: according to WAYBEL_0:def 21 :: thesis: ( x in I & x is_>=_than I )
x <= x ;
hence x in I by A4, Th17; :: thesis: x is_>=_than I
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in I or y <= x )
thus ( not y in I or y <= x ) by A4, Th17; :: thesis: verum