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:72
.= the L_join of L9 . a9,b9 by NAT_LAT:def 16
.= 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:72
.= the L_meet of L9 . a9,b9 by NAT_LAT:def 16
.= a9 "/\" b9 by LATTICES:def 2 ; :: thesis: verum