let P be non empty reflexive RelStr ; :: thesis: ( P is upper-bounded iff the InternalRel of P is upper-bounded )

the carrier of P \/ the carrier of P = the carrier of P ;

then A1: field the InternalRel of P c= the carrier of P by RELSET_1:8;

thus ( P is upper-bounded implies the InternalRel of P is upper-bounded ) :: thesis: ( the InternalRel of P is upper-bounded implies P is upper-bounded )

given x being set such that A3: for y being set st y in field the InternalRel of P holds

[y,x] in the InternalRel of P ; :: according to YELLOW21:def 9 :: thesis: P is upper-bounded

the Element of P <= the Element of P ;

then [ the Element of P, the Element of P] in the InternalRel of P ;

then the Element of P in field the InternalRel of P by RELAT_1:15;

then [ the Element of P,x] in the InternalRel of P by A3;

then x in field the InternalRel of P by RELAT_1:15;

then reconsider x = x as Element of P by A1;

take x ; :: according to YELLOW_0:def 5 :: thesis: the carrier of P is_<=_than x

let y be Element of P; :: according to LATTICE3:def 9 :: thesis: ( not y in the carrier of P or y <= x )

y <= y ;

then [y,y] in the InternalRel of P ;

then y in field the InternalRel of P by RELAT_1:15;

then [y,x] in the InternalRel of P by A3;

hence ( not y in the carrier of P or y <= x ) ; :: thesis: verum

the carrier of P \/ the carrier of P = the carrier of P ;

then A1: field the InternalRel of P c= the carrier of P by RELSET_1:8;

thus ( P is upper-bounded implies the InternalRel of P is upper-bounded ) :: thesis: ( the InternalRel of P is upper-bounded implies P is upper-bounded )

proof

set y = the Element of P;
given x being Element of P such that A2:
x is_>=_than the carrier of P
; :: according to YELLOW_0:def 5 :: thesis: the InternalRel of P is upper-bounded

take x ; :: according to YELLOW21:def 9 :: thesis: for y being set st y in field the InternalRel of P holds

[y,x] in the InternalRel of P

let y be set ; :: thesis: ( y in field the InternalRel of P implies [y,x] in the InternalRel of P )

assume y in field the InternalRel of P ; :: thesis: [y,x] in the InternalRel of P

then reconsider y = y as Element of P by A1;

x >= y by A2;

hence [y,x] in the InternalRel of P ; :: thesis: verum

end;take x ; :: according to YELLOW21:def 9 :: thesis: for y being set st y in field the InternalRel of P holds

[y,x] in the InternalRel of P

let y be set ; :: thesis: ( y in field the InternalRel of P implies [y,x] in the InternalRel of P )

assume y in field the InternalRel of P ; :: thesis: [y,x] in the InternalRel of P

then reconsider y = y as Element of P by A1;

x >= y by A2;

hence [y,x] in the InternalRel of P ; :: thesis: verum

given x being set such that A3: for y being set st y in field the InternalRel of P holds

[y,x] in the InternalRel of P ; :: according to YELLOW21:def 9 :: thesis: P is upper-bounded

the Element of P <= the Element of P ;

then [ the Element of P, the Element of P] in the InternalRel of P ;

then the Element of P in field the InternalRel of P by RELAT_1:15;

then [ the Element of P,x] in the InternalRel of P by A3;

then x in field the InternalRel of P by RELAT_1:15;

then reconsider x = x as Element of P by A1;

take x ; :: according to YELLOW_0:def 5 :: thesis: the carrier of P is_<=_than x

let y be Element of P; :: according to LATTICE3:def 9 :: thesis: ( not y in the carrier of P or y <= x )

y <= y ;

then [y,y] in the InternalRel of P ;

then y in field the InternalRel of P by RELAT_1:15;

then [y,x] in the InternalRel of P by A3;

hence ( not y in the carrier of P or y <= x ) ; :: thesis: verum