let x be set ; :: thesis: for L being non empty reflexive transitive RelStr holds
( x is Element of (InclPoset (Ids L)) iff x is Ideal of L )
let L be non empty reflexive transitive RelStr ; :: thesis: ( x is Element of (InclPoset (Ids L)) iff x is Ideal of L )

hereby :: thesis: ( x is Ideal of L implies x is Element of (InclPoset (Ids L)) )

assume x is Element of (InclPoset (Ids L)) ; :: thesis: x is Ideal of L
then x in the carrier of (InclPoset (Ids L)) ;
then x in Ids L by YELLOW_1:1;
then ex J being Ideal of L st J = x ;
hence x is Ideal of L ; :: thesis: verum

end;

assume x is Ideal of L ; :: thesis: x is Element of (InclPoset (Ids L))
then x in { Y where Y is Ideal of L : verum } ;
hence x is Element of (InclPoset (Ids L)) by YELLOW_1:1; :: thesis: verum