let R be non empty reflexive antisymmetric RelStr ; :: thesis: for x being Element of R holds (uparrow x) /\ (downarrow x) = {x}
let x be Element of R; :: thesis: (uparrow x) /\ (downarrow x) = {x}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {x} c= (uparrow x) /\ (downarrow x)

let a be set ; :: thesis: ( a in (uparrow x) /\ (downarrow x) implies a in {x} )
assume A1: a in (uparrow x) /\ (downarrow x) ; :: thesis: a in {x}
then reconsider y = a as Element of R ;
( y in uparrow x & y in downarrow x ) by A1, XBOOLE_0:def 4;
then ( x <= y & y <= x ) by WAYBEL_0:17, WAYBEL_0:18;
then x = a by ORDERS_2:25;
hence a in {x} by TARSKI:def 1; :: thesis: verum

end;

x <= x ;
then ( x in uparrow x & x in downarrow x ) by WAYBEL_0:17, WAYBEL_0:18;
then x in (uparrow x) /\ (downarrow x) by XBOOLE_0:def 4;
hence {x} c= (uparrow x) /\ (downarrow x) by ZFMISC_1:37; :: thesis: verum