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 LemMinFunc01;
take a ; :: thesis: a is_<=_than the carrier of (ConPoset P,Q)
thus a is_<=_than the carrier of (ConPoset P,Q) by ThConPoset02; :: 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 ThConPoset01;
hence ConPoset P,Q is chain-complete by DefchainComplete, A1; :: thesis: verum