let L be non empty LattStr ; :: thesis: for S being non empty SubLattStr of L
for x1, x2 being Element of L
for y1, y2 being Element of S st x1 = y1 & x2 = y2 holds
x1 "\/" x2 = y1 "\/" y2
let S be non empty SubLattStr of L; :: thesis: for x1, x2 being Element of L
for y1, y2 being Element of S st x1 = y1 & x2 = y2 holds
x1 "\/" x2 = y1 "\/" y2
let x1, x2 be Element of L; :: thesis: for y1, y2 being Element of S st x1 = y1 & x2 = y2 holds
x1 "\/" x2 = y1 "\/" y2
let y1, y2 be Element of S; :: thesis: ( x1 = y1 & x2 = y2 implies x1 "\/" x2 = y1 "\/" y2 )
assume Z4: ( x1 = y1 & x2 = y2 ) ; :: thesis: x1 "\/" x2 = y1 "\/" y2
Z5: the L_join of S = the L_join of L || the carrier of S by Defx1
.= the L_join of L | [: the carrier of S, the carrier of S:] ;
[y1,y2] in [: the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
hence x1 "\/" x2 = y1 "\/" y2 by Z4, Z5, FUNCT_1:49; :: thesis: verum