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

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

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

A1: downarrow (downarrow X) c= downarrow X

proof

downarrow X c= downarrow (downarrow X)
by WAYBEL_0:16;
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;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

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