let p, r, s, q be ext-real number ; :: thesis: ( p <= r & p <= s & r <= q & s <= q implies ([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = [.p,q.] )
assume that
A1: p <= r and
A2: p <= s and
A3: r <= q and
A4: s <= q ; :: thesis: ([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = [.p,q.]

per cases ( r <= s or s < r ) ;

suppose r <= s ; :: thesis: ([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = [.p,q.]

hence ([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = [.p,s.] \/ ].s,q.] by A1, Th166
.= [.p,q.] by A2, A4, Th167 ;
:: thesis: verum

end;

suppose A5: s < r ; :: thesis: ([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = [.p,q.]

hence ([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = ([.p,r.[ \/ {} ) \/ ].s,q.] by Th29
.= [.p,q.] by A2, A3, A5, Th175 ;
:: thesis: verum

end;

end;