let S, T be antisymmetric with_suprema 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 Th14
.= x2 "\/" ([y1,y2] `2)
.= x2 "\/" y2
.= [(x1 "\/" y1),(x2 "\/" y2)] `2 ;
([x1,x2] "\/" [y1,y2]) `1 = ([x1,x2] `1) "\/" ([y1,y2] `1) by Th14
.= 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