let C be complete Lattice; :: thesis: for a being Element of C
for X being set holds
( a = "/\" X,C iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) ) )
let a be Element of C; :: thesis: for X being set holds
( a = "/\" X,C iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) ) )
let X be set ; :: thesis: ( a = "/\" X,C iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) ) )
set Y = { b where b is Element of C : b is_less_than X } ;
A1: ( a = "/\" X,C iff ( { b where b is Element of C : b is_less_than X } is_less_than a & ( for c being Element of C st { b where b is Element of C : b is_less_than X } is_less_than c holds
a [= c ) ) ) by Def21;
thus ( a = "/\" X,C implies ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) ) ) :: thesis: ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) implies a = "/\" X,C )

proof

assume A2: a = "/\" X,C ; :: thesis: ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) )
then A3: ( { b where b is Element of C : b is_less_than X } is_less_than a & ( for c being Element of C st { b where b is Element of C : b is_less_than X } is_less_than c holds
a [= c ) ) by Def21;
thus a is_less_than X :: thesis: for b being Element of C st b is_less_than X holds
b [= a

proof

let b be Element of C; :: according to LATTICE3:def 16 :: thesis: ( b in X implies a [= b )
assume A4: b in X ; :: thesis: a [= b
{ b where b is Element of C : b is_less_than X } is_less_than b

proof

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

end;

hence a [= b by A2, Def21; :: thesis: verum

end;

let b be Element of C; :: thesis: ( b is_less_than X implies b [= a )
assume b is_less_than X ; :: thesis: b [= a
then b in { b where b is Element of C : b is_less_than X } ;
hence b [= a by A3, Def17; :: thesis: verum

end;

assume A5: ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) ) ; :: thesis: a = "/\" X,C
A6: { b where b is Element of C : b is_less_than X } is_less_than a

proof

let b be Element of C; :: according to LATTICE3:def 17 :: thesis: ( b in { b where b is Element of C : b is_less_than X } implies b [= a )
assume b in { b where b is Element of C : b is_less_than X } ; :: thesis: b [= a
then ex c being Element of C st
( b = c & c is_less_than X ) ;
hence b [= a by A5; :: thesis: verum

end;

a in { b where b is Element of C : b is_less_than X } by A5;
hence a = "/\" X,C by A1, A6, Def17; :: thesis: verum