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]) `2 = ([x1,x2] `2) "/\" ([y1,y2] `2) by Th13
.= x2 "/\" ([y1,y2] `2)
.= x2 "/\" y2
.= [(x1 "/\" y1),(x2 "/\" y2)] `2 ;
([x1,x2] "/\" [y1,y2]) `1 = ([x1,x2] `1) "/\" ([y1,y2] `1) by Th13
.= x1 "/\" ([y1,y2] `1)
.= x1 "/\" y1
.= [(x1 "/\" y1),(x2 "/\" y2)] `1 ;
hence [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2] by A1, A2, DOMAIN_1:2; :: thesis: verum