q . O in rng q by A1, FUNCT_1:def 3;
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 Def13;
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 ;
A c= ConsecutiveSet (A,O) by Th24;
then reconsider x = x, y = y as Element of ConsecutiveSet (A,O) ;
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