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 object 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 object ; :: 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
A1: ( 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 A1;
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 object 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 object ; :: 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 A2: ( 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
A3: ( 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
A4: ( f in F & a = f . p ) by A3;
consider b being Element of Q such that
A5: ( y = b & ex g being continuous Function of P,Q st
( g in F & b = g . p ) ) by A2;
consider g being continuous Function of P,Q such that
A6: ( g in F & b = g . p ) by A5;
set S = the InternalRel of (ConPoset (P,Q));
A7: the InternalRel of (ConPoset (P,Q)) is_strongly_connected_in F by ORDERS_2:def 7;
per cases ( [f,g] in the InternalRel of (ConPoset (P,Q)) or [g,f] in the InternalRel of (ConPoset (P,Q)) ) by A7, A4, A6, RELAT_2:def 7;
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
A8: ( f = f1 & g = g1 & f1 <= g1 ) by Def7;
a <= b by A8, A4, A6, YELLOW_2:9;
hence ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) by A3, A5, ORDERS_2:def 5; :: 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
A9: ( g = g1 & f = f1 & g1 <= f1 ) by Def7;
b <= a by A9, A4, A6, YELLOW_2:9;
hence ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) by A3, A5, ORDERS_2:def 5; :: thesis: verum
end;
end;
end;
then A10: the InternalRel of Q is_connected_in IT by RELAT_2:def 6;
for x being object st x in IT holds
[x,x] in the InternalRel of Q
proof
let x be object ; :: 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 5; :: 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 A10, ORDERS_1:7;
then reconsider IT = IT as Chain of Q by ORDERS_2:def 7;
consider a being object such that
A11: a in F by XBOOLE_0:7;
a in ConFuncs (P,Q) by A11;
then consider b being Element of Funcs ( the carrier of P, the carrier of Q) such that
A12: ( a = b & ex f being continuous Function of P,Q st f = b ) ;
consider f being continuous Function of P,Q such that
A13: f = b by A12;
reconsider c = f . p as Element of Q ;
c in IT by A11, A12, A13;
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