let A be RelStr ; :: thesis: ( A is with_suprema implies not A is empty )
assume A1: 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 10 :: thesis: not A is empty
consider x, y being Element of ;
consider z being Element of such that
A2: x <= z and
y <= z and
for z' being Element of st x <= z' & y <= z' holds
z <= z' by A1;
[x,z] in the InternalRel of A by A2, ORDERS_2:def 9;
hence not A is empty ; :: thesis: verum