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

proof

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

end;

Filt L c= Ids (L opp)

proof

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

end;

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