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 downarrow x by A1, XBOOLE_0:def 4;
then A2: y <= x by WAYBEL_0:17;
y in uparrow x by A1, XBOOLE_0:def 4;
then x <= y by WAYBEL_0:18;
then x = a by A2, ORDERS_2:2;
hence a in {x} by TARSKI:def 1; :: thesis: verum

end;

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