let N be non empty reflexive RelStr ; :: thesis: for x being Element of N holds (uparrow x) ^0 = wayabove x
let x be Element of N; :: thesis: (uparrow x) ^0 = wayabove x
thus (uparrow x) ^0 c= wayabove x :: according to XBOOLE_0:def 10 :: thesis: wayabove x c= (uparrow x) ^0

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (uparrow x) ^0 or a in wayabove x )
assume a in (uparrow x) ^0 ; :: thesis: a in wayabove x
then consider u being Element of N such that
A1: a = u and
A2: for D being non empty directed Subset of N st u <= sup D holds
uparrow x meets D ;
u >> x

proof

let D be non empty directed Subset of N; :: according to WAYBEL_3:def 1 :: thesis: ( not u <= "\/" (D,N) or ex b₁ being Element of the carrier of N st
( b₁ in D & x <= b₁ ) )
assume u <= sup D ; :: thesis: ex b₁ being Element of the carrier of N st
( b₁ in D & x <= b₁ )
then uparrow x meets D by A2;
then consider d being object such that
A3: d in (uparrow x) /\ D by XBOOLE_0:4;
reconsider d = d as Element of N by A3;
take d ; :: thesis: ( d in D & x <= d )
thus d in D by A3, XBOOLE_0:def 4; :: thesis: x <= d
d in uparrow x by A3, XBOOLE_0:def 4;
hence x <= d by WAYBEL_0:18; :: thesis: verum

end;

hence a in wayabove x by A1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in wayabove x or a in (uparrow x) ^0 )
assume A4: a in wayabove x ; :: thesis: a in (uparrow x) ^0
then reconsider b = a as Element of N ;

now :: thesis: for D being non empty directed Subset of N st b <= sup D holds
uparrow x meets D

A5: b >> x by A4, WAYBEL_3:8;
let D be non empty directed Subset of N; :: thesis: ( b <= sup D implies uparrow x meets D )
assume b <= sup D ; :: thesis: uparrow x meets D
then consider d being Element of N such that
A6: d in D and
A7: x <= d by A5;
d in uparrow x by A7, WAYBEL_0:18;
hence uparrow x meets D by A6, XBOOLE_0:3; :: thesis: verum

end;

hence a in (uparrow x) ^0 ; :: thesis: verum