set ab = subrelstr [#a,b#];
let x, y be Element of L; :: according to YELLOW_0:def 17 :: thesis: ( not x in the carrier of (subrelstr [#a,b#]) or not y in the carrier of (subrelstr [#a,b#]) or not ex_sup_of {x,y},L or "\/" {x,y},L in the carrier of (subrelstr [#a,b#]) )
assume ( x in the carrier of (subrelstr [#a,b#]) & y in the carrier of (subrelstr [#a,b#]) & ex_sup_of {x,y},L ) ; :: thesis: "\/" {x,y},L in the carrier of (subrelstr [#a,b#])
then ( x in [#a,b#] & y in [#a,b#] ) by YELLOW_0:def 15;
then A1: ( x <= b & y <= b & a <= x & a <= y ) by Def4;
A2: sup {x,y} = x "\/" y by YELLOW_0:41;
then ( x <= sup {x,y} & y <= sup {x,y} ) by YELLOW_0:22;
then A3: a <= sup {x,y} by A1, YELLOW_0:def 2;
sup {x,y} <= b by A1, A2, YELLOW_0:22;
then sup {x,y} in [#a,b#] by A3, Def4;
hence "\/" {x,y},L in the carrier of (subrelstr [#a,b#]) by YELLOW_0:def 15; :: thesis: verum