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 LATTICE5:def 14;
then consider x, y being Element of A, a, b being Element of L such that
A2: ( q . O = [x,y,a,b] & d . x,y <= a "\/" b ) ;
A3: ( x in A & y in A ) ;
A c= ConsecutiveSet2 A,O by Th18;
then reconsider x = x, y = y as Element of ConsecutiveSet2 A,O by A3;
reconsider a = a, b = b as Element of L ;
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:] ; :: thesis: verum