let x, y be Element of L; :: according to YELLOW_0:def 16 :: thesis: ( 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 ; :: thesis: "/\" ({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; :: thesis: verum

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 ; :: thesis: "/\" ({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; :: thesis: verum