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

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

let x be Element 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 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;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

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