let X be set ; :: according to LATTICE3:def 18 :: thesis:
consider a being Element of A such that
A2: X is_<=_than a and
A3: for b being Element of A st X is_<=_than b holds
a <= b by Def12;
reconsider a9 = a as Element of (LattPOSet (latt A)) by A1;
take p = % a9; :: thesis:
A4: p % = p ;
thus X is_less_than p :: thesis:

let q be Element of (latt A); :: according to LATTICE3:def 17 :: thesis:
reconsider b = q as Element of A by A1;
assume q in X ; :: thesis:
then b <= a by A2;
then [b,a] in the InternalRel of A ;
then q % <= a9 by A1;
hence q [= p by A4, Th7; :: thesis:

end;

let c be Element of A; :: according to LATTICE3:def 9 :: thesis:
reconsider c9 = c as Element of (LattPOSet (latt A)) by A1;
assume c in X ; :: thesis:
then c9 <= q % by A5;
then [c,b] in the InternalRel of RelStr(# the carrier of A, the InternalRel of A #) by A1;
hence c <= b ; :: thesis:

end;

end;