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#]) )
set ab = subrelstr [#a,b#];
assume that
A1: x in the carrier of (subrelstr [#a,b#]) and
A2: y in the carrier of (subrelstr [#a,b#]) and
ex_sup_of {x,y},L ; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr [#a,b#])
A3: x in [#a,b#] by A1, YELLOW_0:def 15;
then A4: a <= x by Def4;
A5: sup {x,y} = x "\/" y by YELLOW_0:41;
then x <= sup {x,y} by YELLOW_0:22;
then A6: a <= sup {x,y} by A4, YELLOW_0:def 2;
y in [#a,b#] by A2, YELLOW_0:def 15;
then A7: y <= b by Def4;
x <= b by A3, Def4;
then sup {x,y} <= b by A7, A5, YELLOW_0:22;
then sup {x,y} in [#a,b#] by A6, Def4;
hence "\/" ({x,y},L) in the carrier of (subrelstr [#a,b#]) by YELLOW_0:def 15; :: thesis: verum