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 A2: c in {a,b} ; :: thesis: c [= a "\/" b
A3: a [= a "\/" b by LATTICES:5;
b [= b "\/" a by LATTICES:5;
hence c [= a "\/" b by A2, A3, TARSKI:def 2; :: thesis: verum
end;
A4: a in {a,b} by TARSKI:def 2;
A5: b in {a,b} by TARSKI:def 2;
now :: thesis: for c being Element of C st {a,b} is_less_than c holds
a "\/" b [= c
let c be Element of C; :: thesis: ( {a,b} is_less_than c implies a "\/" b [= c )
assume A6: {a,b} is_less_than c ; :: thesis: a "\/" b [= c
then A7: a [= c by A4;
b [= c by A5, A6;
hence a "\/" b [= c by A7, 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:6; :: thesis: verum
end;
then A8: 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 A9: ex c being Element of C st
( d = c & c is_less_than {a,b} ) ;
then A10: d [= a by A4;
d [= b by A5, A9;
hence d [= a "/\" b by A10, FILTER_0:7; :: thesis: verum
end;
hence a "/\" b = "/\" {a,b} by A8, Th40; :: thesis: verum