let L be non empty complete Poset; :: thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R st C is maximal holds
subrelstr C is complete
let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: for C being non empty strict_chain of R st C is maximal holds
subrelstr C is complete
let C be non empty strict_chain of R; :: thesis: ( C is maximal implies subrelstr C is complete )
assume A1: C is maximal ; :: thesis: subrelstr C is complete
for X being Subset of (subrelstr C) holds ex_sup_of X, subrelstr C
proof
let X be Subset of (subrelstr C); :: thesis: ex_sup_of X, subrelstr C
X is Subset of C by YELLOW_0:def 15;
hence ex_sup_of X, subrelstr C by A1, Th8, YELLOW_0:17; :: thesis: verum
end;
hence subrelstr C is complete by YELLOW_0:53; :: thesis: verum