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

hence uparrow (uparrow X) = uparrow X by A1; :: thesis: verum

let X be Subset of L; :: thesis: uparrow (uparrow X) = uparrow X

A1: uparrow (uparrow X) c= uparrow X

proof

uparrow X c= uparrow (uparrow X)
by WAYBEL_0:16;
let x be object ; :: 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;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

hence uparrow (uparrow X) = uparrow X by A1; :: thesis: verum