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