let A be RelStr ; ( A is with_suprema implies not A is empty )
assume A1:
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 ) )
; LATTICE3:def 10 not A is empty
set x = the Element of A;
consider z being Element of A such that
A2:
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 A1;
[ the Element of A,z] in the InternalRel of A
by A2;
hence
not A is empty
; verum