let S, T be antisymmetric with_infima RelStr ; :: thesis: for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]
let x1, y1 be Element of S; :: thesis: for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]
let x2, y2 be Element of T; :: thesis: [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
A2: ([x1,x2] "/\" [y1,y2]) `1 = ([x1,x2] `1 ) "/\" ([y1,y2] `1 ) by Th13
.= x1 "/\" ([y1,y2] `1 ) by MCART_1:7
.= x1 "/\" y1 by MCART_1:7
.= [(x1 "/\" y1),(x2 "/\" y2)] `1 by MCART_1:7 ;
([x1,x2] "/\" [y1,y2]) `2 = ([x1,x2] `2 ) "/\" ([y1,y2] `2 ) by Th13
.= x2 "/\" ([y1,y2] `2 ) by MCART_1:7
.= x2 "/\" y2 by MCART_1:7
.= [(x1 "/\" y1),(x2 "/\" y2)] `2 by MCART_1:7 ;
hence [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2] by A1, A2, DOMAIN_1:12; :: thesis: verum