let L be Lattice; for L9 being SubLattice of L
for a, b being Element of L
for a9, b9 being Element of L9 st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
let L9 be SubLattice of L; for a, b being Element of L
for a9, b9 being Element of L9 st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
let a, b be Element of L; for a9, b9 being Element of L9 st a = a9 & b = b9 holds
( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
let a9, b9 be Element of L9; ( a = a9 & b = b9 implies ( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 ) )
assume A1:
( a = a9 & b = b9 )
; ( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 )
thus a "\/" b =
the L_join of L . (a,b)
by LATTICES:def 1
.=
( the L_join of L || the carrier of L9) . [a9,b9]
by A1, FUNCT_1:49
.=
the L_join of L9 . (a9,b9)
by NAT_LAT:def 12
.=
a9 "\/" b9
by LATTICES:def 1
; a "/\" b = a9 "/\" b9
thus a "/\" b =
the L_meet of L . (a,b)
by LATTICES:def 2
.=
( the L_meet of L || the carrier of L9) . [a9,b9]
by A1, FUNCT_1:49
.=
the L_meet of L9 . (a9,b9)
by NAT_LAT:def 12
.=
a9 "/\" b9
by LATTICES:def 2
; verum