let L be non empty reflexive transitive RelStr ; :: thesis: Ids L = Filt (L opp )
A1: Ids L c= Filt (L opp )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ids L or x in Filt (L opp ) )
assume x in Ids L ; :: thesis: x in Filt (L opp )
then x in { X where X is Ideal of L : verum } by WAYBEL_0:def 23;
then consider x1 being Ideal of L such that
A2: x1 = x ;
A3: x1 is upper Subset of (L opp ) by YELLOW_7:28;
x1 is filtered Subset of (L opp ) by YELLOW_7:26;
then x in { X where X is Filter of (L opp ) : verum } by A2, A3;
hence x in Filt (L opp ) by WAYBEL_0:def 24; :: thesis: verum

end;

Filt (L opp ) c= Ids L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Filt (L opp ) or x in Ids L )
assume x in Filt (L opp ) ; :: thesis: x in Ids L
then x in { X where X is Filter of (L opp ) : verum } by WAYBEL_0:def 24;
then consider x1 being Filter of (L opp ) such that
A4: x1 = x ;
A5: x1 is lower Subset of L by YELLOW_7:28;
x1 is directed Subset of L by YELLOW_7:26;
then x in { X where X is Ideal of L : verum } by A4, A5;
hence x in Ids L by WAYBEL_0:def 23; :: thesis: verum

end;

hence Ids L = Filt (L opp ) by A1, XBOOLE_0:def 10; :: thesis: verum