let C be complete Lattice; :: thesis: for a being Element of C holds
( "\/" {a} = a & "/\" {a} = a )
let a be Element of C; :: thesis: ( "\/" {a} = a & "/\" {a} = a )
A1: a in {a} by TARSKI:def 1;
{a} is_less_than a
proof
let b be Element of C; :: according to LATTICE3:def 17 :: thesis: ( b in {a} implies b [= a )
assume b in {a} ; :: thesis: b [= a
hence b [= a by TARSKI:def 1; :: thesis: verum
end;
hence "\/" {a} = a by A1, Th40; :: thesis: "/\" {a} = a
a is_less_than {a}
proof
let b be Element of C; :: according to LATTICE3:def 16 :: thesis: ( b in {a} implies a [= b )
assume b in {a} ; :: thesis: a [= b
hence a [= b by TARSKI:def 1; :: thesis: verum
end;
hence "/\" {a} = a by A1, Th41; :: thesis: verum