let L be non empty LattStr ; 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; 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; for y1, y2 being Element of S st x1 = y1 & x2 = y2 holds
x1 "/\" x2 = y1 "/\" y2
let y1, y2 be Element of S; ( x1 = y1 & x2 = y2 implies x1 "/\" x2 = y1 "/\" y2 )
assume Z4:
( x1 = y1 & x2 = y2 )
; x1 "/\" x2 = y1 "/\" y2
Z5: the L_meet of S =
the L_meet of L || the carrier of S
by Defx1
.=
the L_meet 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; verum