let S, T be antisymmetric with_suprema RelStr ; 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; for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]
let x2, y2 be Element of T; [(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; verum