let A be RelStr ; :: thesis: ( A is with_infima implies not A is empty )
assume A3: for x, y being Element of A ex z being Element of A st
( x >= z & y >= z & ( for z9 being Element of A st x >= z9 & y >= z9 holds
z >= z9 ) ) ; :: according to LATTICE3:def 11 :: thesis: not A is empty
set x = the Element of A;
consider z being Element of A such that
A4: the Element of A >= z and
the Element of A >= z and
for z9 being Element of A st the Element of A >= z9 & the Element of A >= z9 holds
z >= z9 by A3;
[z, the Element of A] in the InternalRel of A by A4;
hence not A is empty ; :: thesis: verum