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