let x be set ; :: thesis: for p, q being ext-real number st x in ].p,q.[ holds
( x in [.p,q.] & x <> p & x <> q )
let p, q be ext-real number ; :: thesis: ( x in ].p,q.[ implies ( x in [.p,q.] & x <> p & x <> q ) )
assume x in ].p,q.[ ; :: thesis: ( x in [.p,q.] & x <> p & x <> q )
then ( x in ].p,q.] & x <> q ) by Th15;
hence ( x in [.p,q.] & x <> p & x <> q ) by Th12; :: thesis: verum