let L be non empty reflexive transitive RelStr ; :: thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds
SupBelow (R,C) is strict_chain of R
let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: for C being strict_chain of R st ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) holds
SupBelow (R,C) is strict_chain of R
let C be strict_chain of R; :: thesis: ( ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) implies SupBelow (R,C) is strict_chain of R )
assume A1: for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ; :: thesis: SupBelow (R,C) is strict_chain of R
thus SupBelow (R,C) is strict_chain of R :: thesis: verum

proof

let a, b be set ; :: according to WAYBEL35:def 3 :: thesis: ( a in SupBelow (R,C) & b in SupBelow (R,C) & not [a,b] in R & not a = b implies [b,a] in R )
assume A2: a in SupBelow (R,C) ; :: thesis: ( not b in SupBelow (R,C) or [a,b] in R or a = b or [b,a] in R )
then A3: a = sup (SetBelow (R,C,a)) by Def10;
reconsider a = a as Element of L by A2;
A4: a <= a ;
A5: ex_sup_of SetBelow (R,C,a),L by A1;
assume A6: b in SupBelow (R,C) ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )
then A7: b = sup (SetBelow (R,C,b)) by Def10;
reconsider b = b as Element of L by A6;
A8: b <= b ;
A9: ex_sup_of SetBelow (R,C,b),L by A1;

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

hence ( [a,b] in R or a = b or [b,a] in R ) ; :: thesis: verum

end;

suppose A10: a <> b ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

( ( for x being Element of L st x in C holds
( [x,a] in R iff [x,b] in R ) ) implies a = b )

proof

assume A11: for x being Element of L st x in C holds
( [x,a] in R iff [x,b] in R ) ; :: thesis: a = b
SetBelow (R,C,a) = SetBelow (R,C,b)

proof

thus SetBelow (R,C,a) c= SetBelow (R,C,b) :: according to XBOOLE_0:def 10 :: thesis: SetBelow (R,C,b) c= SetBelow (R,C,a)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SetBelow (R,C,a) or x in SetBelow (R,C,b) )
assume A12: x in SetBelow (R,C,a) ; :: thesis: x in SetBelow (R,C,b)
then reconsider x = x as Element of L ;
A13: x in C by A12, Th15;
[x,a] in R by A12, Th15;
then [x,b] in R by A13, A11;
hence x in SetBelow (R,C,b) by A13, Th15; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SetBelow (R,C,b) or x in SetBelow (R,C,a) )
assume A14: x in SetBelow (R,C,b) ; :: thesis: x in SetBelow (R,C,a)
then reconsider x = x as Element of L ;
A15: x in C by A14, Th15;
[x,b] in R by A14, Th15;
then [x,a] in R by A15, A11;
hence x in SetBelow (R,C,a) by A15, Th15; :: thesis: verum

end;

hence a = b by A2, A7, Def10; :: thesis: verum

end;

then consider x being Element of L such that
A16: x in C and
A17: ( ( [x,a] in R & not [x,b] in R ) or ( not [x,a] in R & [x,b] in R ) ) by A10;
A18: x <= x ;
thus ( [a,b] in R or a = b or [b,a] in R ) :: thesis: verum

proof

per cases ( ( [x,a] in R & not [x,b] in R ) or ( not [x,a] in R & [x,b] in R ) ) by A17;

suppose that A19: [x,a] in R and
A20: not [x,b] in R ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

SetBelow (R,C,b) is_<=_than x

proof

let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in SetBelow (R,C,b) or y <= x )
assume A21: y in SetBelow (R,C,b) ; :: thesis: y <= x
then [y,b] in R by Th15;
then A22: y <= b by WAYBEL_4:def 3;
y in C by A21, Th15;
then ( [y,x] in R or x = y or [x,y] in R ) by A16, Def3;
hence y <= x by A18, A20, A22, WAYBEL_4:def 3, WAYBEL_4:def 4; :: thesis: verum

end;

then b <= x by A7, A9, YELLOW_0:def 9;
hence ( [a,b] in R or a = b or [b,a] in R ) by A4, A19, WAYBEL_4:def 4; :: thesis: verum

end;

suppose that A23: not [x,a] in R and
A24: [x,b] in R ; :: thesis: ( [a,b] in R or a = b or [b,a] in R )

SetBelow (R,C,a) is_<=_than x

proof

let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in SetBelow (R,C,a) or y <= x )
assume A25: y in SetBelow (R,C,a) ; :: thesis: y <= x
then [y,a] in R by Th15;
then A26: y <= a by WAYBEL_4:def 3;
y in C by A25, Th15;
then ( [y,x] in R or x = y or [x,y] in R ) by A16, Def3;
hence y <= x by A18, A23, A26, WAYBEL_4:def 3, WAYBEL_4:def 4; :: thesis: verum

end;

then a <= x by A3, A5, YELLOW_0:def 9;
hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A24, WAYBEL_4:def 4; :: thesis: verum

end;

end;

end;

end;

end;

end;