q . O in rng q by A1, FUNCT_1:def 5;
then q . O in { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } by Def14;
then consider x, y being Element of A, a, b being Element of L such that
A2: q . O = [x,y,a,b] and
d . x,y <= a "\/" b ;
reconsider a = a, b = b as Element of L ;
A3: ( x in A & y in A ) ;
A c= ConsecutiveSet A,O by Th27;
then reconsider x = x, y = y as Element of ConsecutiveSet A,O by A3;
reconsider z = [x,y,a,b] as Element of [:(ConsecutiveSet A,O),(ConsecutiveSet A,O),the carrier of L,the carrier of L:] ;
z = q . O by A2;
hence q . O is Element of [:(ConsecutiveSet A,O),(ConsecutiveSet A,O),the carrier of L,the carrier of L:] ; :: thesis: verum