let x, y be Element of L; YELLOW_0:def 16 ( not x in the carrier of (subrelstr [#a,b#]) or not y in the carrier of (subrelstr [#a,b#]) or not ex_inf_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_inf_of {x,y},L
; "/\" ({x,y},L) in the carrier of (subrelstr [#a,b#])
A3:
x in [#a,b#]
by A1, YELLOW_0:def 15;
then A4:
x <= b
by Def4;
A5:
inf {x,y} = x "/\" y
by YELLOW_0:40;
then
inf {x,y} <= x
by YELLOW_0:23;
then A6:
inf {x,y} <= b
by A4, YELLOW_0:def 2;
y in [#a,b#]
by A2, YELLOW_0:def 15;
then A7:
a <= y
by Def4;
a <= x
by A3, Def4;
then
a <= inf {x,y}
by A7, A5, YELLOW_0:23;
then
inf {x,y} in [#a,b#]
by A6, Def4;
hence
"/\" ({x,y},L) in the carrier of (subrelstr [#a,b#])
by YELLOW_0:def 15; verum