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 set ; :: 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 & ( 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 A1;
then consider d being set such that
A2: d in (uparrow x) /\ D by XBOOLE_0:4;
reconsider d = d as Element of N by A2;
take d ; :: thesis: ( d in D & x <= d )
thus d in D by A2, XBOOLE_0:def 4; :: thesis: x <= d
d in uparrow x by A2, 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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in wayabove x or a in (uparrow x) ^0 )
assume A3: a in wayabove x ; :: thesis: a in (uparrow x) ^0
then reconsider b = a as Element of N ;

now

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

end;

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