let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
let f be Function of X,Y; :: thesis: for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
let g be Function of Y,X; :: thesis: ex Xa, Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
deffunc H1( set ) -> Element of bool X = X \ (g .: (Y \ (f .: $1)));
A1: for x being set st x in bool X holds
H1(x) in bool X ;
consider h being Function of (bool X),(bool X) such that
A2: for x being set st x in bool X holds
h . x = H1(x) from FUNCT_2:sch 11(A1);
now :: thesis: for x, y being set st x in dom h & y in dom h & x c= y holds
h . x c= h . y
let x, y be set ; :: thesis: ( x in dom h & y in dom h & x c= y implies h . x c= h . y )
assume that
A3: x in dom h and
A4: y in dom h and
A5: x c= y ; :: thesis: h . x c= h . y
f .: x c= f .: y by A5, RELAT_1:123;
then Y \ (f .: y) c= Y \ (f .: x) by XBOOLE_1:34;
then g .: (Y \ (f .: y)) c= g .: (Y \ (f .: x)) by RELAT_1:123;
then X \ (g .: (Y \ (f .: x))) c= X \ (g .: (Y \ (f .: y))) by XBOOLE_1:34;
then h . x c= X \ (g .: (Y \ (f .: y))) by A2, A3;
hence h . x c= h . y by A2, A4; :: thesis: verum
end;
then reconsider h = h as V224() Function of (bool X),(bool X) by COHSP_1:def 11;
take Xa = lfp (X,h); :: thesis: ex Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
take Xb = X \ Xa; :: thesis: ex Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
take Ya = f .: Xa; :: thesis: ex Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
take Yb = Y \ Ya; :: thesis: ( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus Xa misses Xb by XBOOLE_1:79; :: thesis: ( Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus Ya misses Yb by XBOOLE_1:79; :: thesis: ( Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus Xa \/ Xb = X by XBOOLE_1:45; :: thesis: ( Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus Ya \/ Yb = Y by XBOOLE_1:45; :: thesis: ( f .: Xa = Ya & g .: Yb = Xb )
thus f .: Xa = Ya ; :: thesis: g .: Yb = Xb
A6: Xa is_a_fixpoint_of h by Th4;
thus g .: Yb = X /\ (g .: (Y \ (f .: Xa))) by XBOOLE_1:28
.= X \ (X \ (g .: (Y \ (f .: Xa)))) by XBOOLE_1:48
.= X \ (h . Xa) by A2
.= Xb by A6 ; :: thesis: verum