let a, b be Real; ( a <= b implies {a,b} c= [.a,b.] )
assume A1:
a <= b
; {a,b} c= [.a,b.]
let x be object ; TARSKI:def 3 ( not x in {a,b} or x in [.a,b.] )
assume
x in {a,b}
; x in [.a,b.]
then
( x = a or x = b )
by TARSKI:def 2;
hence
x in [.a,b.]
by A1, XXREAL_1:1; verum