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

proof

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

end;

Ids (L opp ) c= Filt L

proof

let x be set ; :: 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
A4: x1 = x ;
A5: x1 is upper Subset of L by YELLOW_7:29;
x1 is filtered Subset of L by YELLOW_7:27;
then x in { X where X is Filter of L : verum } by A4, A5;
hence x in Filt L by WAYBEL_0:def 24; :: thesis: verum

end;

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