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

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

hence
subrelstr C is complete
by YELLOW_0:53; :: thesis: verum
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;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