let L be non empty reflexive transitive RelStr ; :: thesis: for x being Element of L holds downarrow (downarrow x) = downarrow x
let x be Element of L; :: thesis: downarrow (downarrow x) = downarrow x
A1: downarrow (downarrow x) c= downarrow x

proof

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

end;

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