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 LATTICE5:def 13;
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= ConsecutiveSet2 (A,O)
by Th17;
then reconsider x = x, y = y as Element of ConsecutiveSet2 (A,O) ;
reconsider z = [x,y,a,b] as Element of [:(ConsecutiveSet2 (A,O)),(ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:] ;
z = q . O
by A2;
hence
q . O is Element of [:(ConsecutiveSet2 (A,O)),(ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:]
; verum