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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (uparrow a) /\ (downarrow b) or x in [#a,b#] )
assume A5: x in (uparrow a) /\ (downarrow b) ; :: thesis: x in [#a,b#]
then x in uparrow {a} by XBOOLE_0:def 4;
then x in { z where z is Element of L : ex w being Element of L st
( z >= w & w in {a} ) } by WAYBEL_0:15;
then consider y1 being Element of L such that
A6: x = y1 and
A7: ex w being Element of L st
( y1 >= w & w in {a} ) ;
A8: a <= y1 by A7, TARSKI:def 1;
x in downarrow {b} by A5, XBOOLE_0:def 4;
then 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;
then ex y2 being Element of L st
( x = y2 & ex w being Element of L st
( y2 <= w & w in {b} ) ) ;
then y1 <= b by A6, TARSKI:def 1;
hence x in [#a,b#] by A6, A8, Def4; :: thesis: verum

end;