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

proof

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

end;

uparrow X c= uparrow (uparrow X) by WAYBEL_0:16;
hence uparrow (uparrow X) = uparrow X by A1, XBOOLE_0:def 10; :: thesis: verum