let L be Lattice; :: thesis: for a, b being Element of L st a [= b holds
for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
b9 [= a9
let a, b be Element of L; :: thesis: ( a [= b implies for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
b9 [= a9 )
assume a [= b ; :: thesis: for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
b9 [= a9
then A1: a "\/" b = b ;
let a9, b9 be Element of (L .:); :: thesis: ( a = a9 & b = b9 implies b9 [= a9 )
assume ( a = a9 & b = b9 ) ; :: thesis: b9 [= a9
then b9 "/\" a9 = b9 by A1, Th37;
hence b9 [= a9 by LATTICES:4; :: thesis: verum