let X, Y be non empty set ; 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; 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; 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);
then reconsider h = h as V224() Function of (bool X),(bool X) by COHSP_1:def 11;
take Xa = lfp (X,h); 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; 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; 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; ( 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; ( Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus
Ya misses Yb
by XBOOLE_1:79; ( Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus
Xa \/ Xb = X
by XBOOLE_1:45; ( Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus
Ya \/ Yb = Y
by XBOOLE_1:45; ( f .: Xa = Ya & g .: Yb = Xb )
thus
f .: Xa = Ya
; 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
; verum