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

proof

let x be object ; :: 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
A2: x1 = x ;
( x1 is lower Subset of L & x1 is directed Subset of L ) by YELLOW_7:26, YELLOW_7:28;
then x in { X where X is Ideal of L : verum } by A2;
hence x in Ids L by WAYBEL_0:def 23; :: thesis: verum

end;

Ids L c= Filt (L opp)

proof

let x be object ; :: 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
A3: x1 = x ;
( x1 is upper Subset of (L opp) & x1 is filtered Subset of (L opp) ) by YELLOW_7:26, YELLOW_7:28;
then x in { X where X is Filter of (L opp) : verum } by A3;
hence x in Filt (L opp) by WAYBEL_0:def 24; :: thesis: verum

end;

hence Ids L = Filt (L opp) by A1; :: thesis: verum