let L be GAD_Lattice; :: thesis: for a, b being Element of L st ex c being Element of L st
( a [= c & b [= c ) holds
a "\/" b = b "\/" a
let a, b be Element of L; :: thesis: ( ex c being Element of L st
( a [= c & b [= c ) implies a "\/" b = b "\/" a )
assume A0: ex c being Element of L st
( a [= c & b [= c ) ; :: thesis: a "\/" b = b "\/" a
b "/\" (a "\/" b) = b
proof
consider c being Element of L such that
A1: ( a [= c & b [= c ) by A0;
thus b "/\" (a "\/" b) = (b "/\" a) "\/" (b "/\" b) by LATTICES:def 11
.= (b "/\" a) "\/" b by IMeet
.= (b "/\" a) "\/" (b "/\" c) by A1, LATTICES:def 9
.= b "/\" (a "\/" c) by LATTICES:def 11
.= b by A1, LATTICES:def 9 ; :: thesis: verum
end;
hence a "\/" b = b "\/" a by Th3726; :: thesis: verum