let L be Lattice; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( a = a9 & b = b9 implies ( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 ) )

assume A1: ( a = a9 & b = b9 ) ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( a = a9 & b = b9 implies ( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 ) )

assume A1: ( a = a9 & b = b9 ) ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum