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#]

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

thus
(uparrow a) /\ (downarrow b) c= [#a,b#]
:: thesis: verum
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;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

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;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