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 )

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

( 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 A4:
I = downarrow x
; :: thesis: I is principal
given x being Element of L such that A1:
x in I
and

A2: 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 by A2, Th17; :: according to XBOOLE_0:def 10 :: thesis: downarrow x c= I

let z be object ; :: 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;A2: 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 by A2, Th17; :: according to XBOOLE_0:def 10 :: thesis: downarrow x c= I

let z be object ; :: 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

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