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

a is_less_than {a}

( "\/" {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

hence
"\/" {a} = a
by A1, Th40; :: thesis: "/\" {a} = a
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;assume b in {a} ; :: thesis: b [= a

hence b [= a by TARSKI:def 1; :: thesis: verum

a is_less_than {a}

proof

hence
"/\" {a} = a
by A1, Th41; :: thesis: verum
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;assume b in {a} ; :: thesis: a [= b

hence a [= b by TARSKI:def 1; :: thesis: verum