let L be Lattice; :: thesis: for a, b being Element of L st a [= b holds
for a', b' being Element of (L .: ) st a = a' & b = b' holds
b' [= a'
let a, b be Element of L; :: thesis: ( a [= b implies for a', b' being Element of (L .: ) st a = a' & b = b' holds
b' [= a' )
assume a [= b ; :: thesis: for a', b' being Element of (L .: ) st a = a' & b = b' holds
b' [= a'
then A1: a "\/" b = b by LATTICES:def 3;
let a', b' be Element of (L .: ); :: thesis: ( a = a' & b = b' implies b' [= a' )
assume ( a = a' & b = b' ) ; :: thesis: b' [= a'
then b' "/\" a' = b' by A1, Th52;
hence b' [= a' by LATTICES:21; :: thesis: verum