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