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