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

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

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

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