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

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;

end;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 )
;

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 )

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

end;( [x,a] in R iff [x,b] in R ) ) implies a = b )

proof

then consider x being Element of L such that
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)

end;( [x,a] in R iff [x,b] in R ) ; :: thesis: a = b

SetBelow (R,C,a) = SetBelow (R,C,b)

proof

hence
a = b
by A2, A7, Def10; :: thesis: verum
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)

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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SetBelow (R,C,b) or x in SetBelow (R,C,a) )
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;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

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

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
end;

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

end;

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 )

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

hence ( [a,b] in R or a = b or [b,a] in R ) by A4, A19, WAYBEL_4:def 4; :: thesis: verum

end;proof

then
b <= x
by A7, A9, YELLOW_0:def 9;
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;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

hence ( [a,b] in R or a = b or [b,a] in R ) by A4, A19, WAYBEL_4:def 4; :: thesis: verum

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 )

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

hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A24, WAYBEL_4:def 4; :: thesis: verum

end;proof

then
a <= x
by A3, A5, YELLOW_0:def 9;
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;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

hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A24, WAYBEL_4:def 4; :: thesis: verum