let L be non empty RelStr ; :: thesis: for x being Element of [:L,L:] holds (inf_op L) . x = (x `1 ) "/\" (x `2 )
let x be Element of [:L,L:]; :: thesis: (inf_op L) . x = (x `1 ) "/\" (x `2 )
the carrier of [:L,L:] = [:the carrier of L,the carrier of L:] by YELLOW_3:def 2;
then consider a, b being set such that
A1: ( a in the carrier of L & b in the carrier of L & x = [a,b] ) by ZFMISC_1:def 2;
thus (inf_op L) . x = (inf_op L) . (x `1 ),(x `2 ) by A1, MCART_1:8
.= (x `1 ) "/\" (x `2 ) by Def4 ; :: thesis: verum