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 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;
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