let C be complete Lattice; :: thesis: for a, b being Element of C holds
( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} )
let a, b be Element of C; :: thesis: ( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} )
A1: {a,b} is_less_than a "\/" b

proof

let c be Element of C; :: according to LATTICE3:def 17 :: thesis: ( c in {a,b} implies c [= a "\/" b )
assume c in {a,b} ; :: thesis: c [= a "\/" b
then ( a [= a "\/" b & b [= b "\/" a & b "\/" a = a "\/" b & ( c = a or c = b ) ) by LATTICES:22, TARSKI:def 2;
hence c [= a "\/" b ; :: thesis: verum

end;

A2: ( a in {a,b} & b in {a,b} ) by TARSKI:def 2;

now

let c be Element of C; :: thesis: ( {a,b} is_less_than c implies a "\/" b [= c )
assume {a,b} is_less_than c ; :: thesis: a "\/" b [= c
then ( a [= c & b [= c ) by A2, Def17;
hence a "\/" b [= c by FILTER_0:6; :: thesis: verum

end;

hence a "\/" b = "\/" {a,b} by A1, Def21; :: thesis: a "/\" b = "/\" {a,b}
a "/\" b is_less_than {a,b}

proof

let c be Element of C; :: according to LATTICE3:def 16 :: thesis: ( c in {a,b} implies a "/\" b [= c )
assume c in {a,b} ; :: thesis: a "/\" b [= c
then ( c = a or ( c = b & b "/\" a = a "/\" b ) ) by TARSKI:def 2;
hence a "/\" b [= c by LATTICES:23; :: thesis: verum

end;

then A3: a "/\" b in { c where c is Element of C : c is_less_than {a,b} } ;
{ c where c is Element of C : c is_less_than {a,b} } is_less_than a "/\" b

proof

let d be Element of C; :: according to LATTICE3:def 17 :: thesis: ( d in { c where c is Element of C : c is_less_than {a,b} } implies d [= a "/\" b )
assume d in { c where c is Element of C : c is_less_than {a,b} } ; :: thesis: d [= a "/\" b
then ex c being Element of C st
( d = c & c is_less_than {a,b} ) ;
then ( d [= a & d [= b ) by A2, Def16;
hence d [= a "/\" b by FILTER_0:7; :: thesis: verum

end;

hence a "/\" b = "/\" {a,b} by A3, Th41; :: thesis: verum