let L be reflexive transitive RelStr ; :: thesis: for X being Subset of L holds downarrow (downarrow X) = downarrow X
let X be Subset of L; :: thesis: downarrow (downarrow X) = downarrow X
A1: downarrow (downarrow X) c= downarrow X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow (downarrow X) or x in downarrow X )
assume A2: x in downarrow (downarrow X) ; :: thesis: x in downarrow X
then reconsider x1 = x as Element of L ;
consider y being Element of L such that
A3: y >= x1 and
A4: y in downarrow X by A2, WAYBEL_0:def 15;
consider z being Element of L such that
A5: z >= y and
A6: z in X by A4, WAYBEL_0:def 15;
z >= x1 by A3, A5, YELLOW_0:def 2;
hence x in downarrow X by A6, WAYBEL_0:def 15; :: thesis: verum

end;

downarrow X c= downarrow (downarrow X) by WAYBEL_0:16;
hence downarrow (downarrow X) = downarrow X by A1; :: thesis: verum