let L be non empty reflexive transitive RelStr ; :: thesis: for a, b being Element of L holds [#a,b#] = (uparrow a) /\ (downarrow b)
let a, b be Element of L; :: thesis: [#a,b#] = (uparrow a) /\ (downarrow b)
thus [#a,b#] c= (uparrow a) /\ (downarrow b) :: according to XBOOLE_0:def 10 :: thesis: (uparrow a) /\ (downarrow b) c= [#a,b#]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [#a,b#] or x in (uparrow a) /\ (downarrow b) )
assume A1: x in [#a,b#] ; :: thesis: x in (uparrow a) /\ (downarrow b)
then reconsider y = x as Element of L ;
A2: ( a <= y & y <= b ) by A1, Def4;
( a in {a} & b in {b} ) by TARSKI:def 1;
then ( y in { z where z is Element of L : ex w being Element of L st
( z >= w & w in {a} ) } & y in { z where z is Element of L : ex w being Element of L st
( z <= w & w in {b} ) } ) by A2;
then ( y in uparrow {a} & y in downarrow {b} ) by WAYBEL_0:14, WAYBEL_0:15;
hence x in (uparrow a) /\ (downarrow b) by XBOOLE_0:def 4; :: thesis: verum

end;

thus (uparrow a) /\ (downarrow b) c= [#a,b#] :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (uparrow a) /\ (downarrow b) or x in [#a,b#] )
assume x in (uparrow a) /\ (downarrow b) ; :: thesis: x in [#a,b#]
then ( x in uparrow {a} & x in downarrow {b} ) by XBOOLE_0:def 4;
then A3: ( x in { z where z is Element of L : ex w being Element of L st
( z >= w & w in {a} ) } & x in { z where z is Element of L : ex w being Element of L st
( z <= w & w in {b} ) } ) by WAYBEL_0:14, WAYBEL_0:15;
then consider y1 being Element of L such that
A4: ( x = y1 & ex w being Element of L st
( y1 >= w & w in {a} ) ) ;
ex y2 being Element of L st
( x = y2 & ex w being Element of L st
( y2 <= w & w in {b} ) ) by A3;
then ( a <= y1 & y1 <= b ) by A4, TARSKI:def 1;
hence x in [#a,b#] by A4, Def4; :: thesis: verum

end;