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

proof

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

end;

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