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 )
proof
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;
set y = the Element of P;
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