set R = the InternalRel of Q;
set IT = { x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } ;
for x being set st x in { x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } holds
x in the carrier of Q

proof

let x be set ; :: thesis: ( x in { x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } implies x in the carrier of Q )
assume x in { x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } ; :: thesis: x in the carrier of Q
then consider a being Element of Q such that
B1: ( x = a & ex f being continuous Function of P,Q st
( f in F & a = f . p ) ) ;
reconsider x = x as Element of the carrier of Q by B1;
x in the carrier of Q ;
hence x in the carrier of Q ; :: thesis: verum

end;

then reconsider IT = { x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } as Subset of Q by TARSKI:def 3;
for x, y being set st x in IT & y in IT & x <> y & not [x,y] in the InternalRel of Q holds
[y,x] in the InternalRel of Q

proof

let x, y be set ; :: thesis: ( x in IT & y in IT & x <> y & not [x,y] in the InternalRel of Q implies [y,x] in the InternalRel of Q )
assume B1: ( x in IT & y in IT & x <> y ) ; :: thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q )
then consider a being Element of Q such that
B2: ( x = a & ex f being continuous Function of P,Q st
( f in F & a = f . p ) ) ;
consider f being continuous Function of P,Q such that
B3: ( f in F & a = f . p ) by B2;
consider b being Element of Q such that
B5: ( y = b & ex g being continuous Function of P,Q st
( g in F & b = g . p ) ) by B1;
consider g being continuous Function of P,Q such that
B6: ( g in F & b = g . p ) by B5;
set S = the InternalRel of (ConPoset P,Q);
B9: the InternalRel of (ConPoset P,Q) is_strongly_connected_in F by ORDERS_2:def 11;

per cases ( [f,g] in the InternalRel of (ConPoset P,Q) or [g,f] in the InternalRel of (ConPoset P,Q) ) by B9, RELAT_2:def 7, B3, B6;

suppose [f,g] in the InternalRel of (ConPoset P,Q) ; :: thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q )

then consider f1, g1 being Function of P,Q such that
C1: ( f = f1 & g = g1 & f1 <= g1 ) by DefConRelat;
a <= b by C1, YELLOW_2:10, B3, B6;
hence ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) by B2, B5, ORDERS_2:def 9; :: thesis: verum

end;

suppose [g,f] in the InternalRel of (ConPoset P,Q) ; :: thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q )

then consider g1, f1 being Function of P,Q such that
C2: ( g = g1 & f = f1 & g1 <= f1 ) by DefConRelat;
b <= a by C2, YELLOW_2:10, B3, B6;
hence ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) by B2, B5, ORDERS_2:def 9; :: thesis: verum

end;

end;

end;

then A1: the InternalRel of Q is_connected_in IT by RELAT_2:def 6;
for x being set st x in IT holds
[x,x] in the InternalRel of Q

proof

let x be set ; :: thesis: ( x in IT implies [x,x] in the InternalRel of Q )
assume x in IT ; :: thesis: [x,x] in the InternalRel of Q
then reconsider x = x as Element of Q ;
x <= x ;
hence [x,x] in the InternalRel of Q by ORDERS_2:def 9; :: thesis: verum

end;

then the InternalRel of Q is_reflexive_in IT by RELAT_2:def 1;
then the InternalRel of Q is_strongly_connected_in IT by A1, ORDERS_1:92;
then reconsider IT = IT as Chain of Q by ORDERS_2:def 11;
consider a being set such that
A2: a in F by XBOOLE_0:7;
a in ConFuncs P,Q by A2;
then consider b being Element of Funcs the carrier of P,the carrier of Q such that
A3: ( a = b & ex f being continuous Function of P,Q st f = b ) ;
consider f being continuous Function of P,Q such that
A4: f = b by A3;
reconsider c = f . p as Element of Q ;
c in IT by A2, A3, A4;
hence { x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } is non empty Chain of Q ; :: thesis: verum