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