set IT = ConPoset (P,Q);
ex a being Element of (ConPoset (P,Q)) st a is_<=_than the carrier of (ConPoset (P,Q))

proof

reconsider a = min_func (P,Q) as Element of (ConPoset (P,Q)) by Lm23;
take a ; :: thesis: a is_<=_than the carrier of (ConPoset (P,Q))
thus a is_<=_than the carrier of (ConPoset (P,Q)) by Th12; :: thesis: verum

end;

then A1: ConPoset (P,Q) is lower-bounded by YELLOW_0:def 4;
for L being Chain of (ConPoset (P,Q)) st not L is empty holds
ex_sup_of L, ConPoset (P,Q) by Th11;
hence ConPoset (P,Q) is chain-complete by A1; :: thesis: verum