assume A1: for X being ManySortedSet of holds
( X in F2() iff ( X in F3() & P1[X] ) ) ; :: thesis: F2() c= F3()
consider K being ManySortedSet of such that
A2: K in F2() by PBOOLE:146;
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in F1() or F2() . i c= F3() . i )
assume A3: i in F1() ; :: thesis: F2() . i c= F3() . i
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F2() . i or x in F3() . i )
assume A4: x in F2() . i ; :: thesis: x in F3() . i
dom (K +* (i .--> x)) = F1() by A3, PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A5: dom (i .--> x) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A6: X . i = (i .--> x) . i by A5, FUNCT_4:14
.= x by FUNCOP_1:87 ;
X in F2()
proof
let s be set ; :: according to PBOOLE:def 4 :: thesis: ( not s in F1() or X . s in F2() . s )
assume A7: s in F1() ; :: thesis: X . s in F2() . s
per cases ( s = i or s <> i ) ;
suppose s = i ; :: thesis: X . s in F2() . s
hence X . s in F2() . s by A4, A6; :: thesis: verum
end;
suppose s <> i ; :: thesis: X . s in F2() . s
then not s in dom (i .--> x) by A5, TARSKI:def 1;
then X . s = K . s by FUNCT_4:12;
hence X . s in F2() . s by A2, A7, PBOOLE:def 4; :: thesis: verum
end;
end;
end;
then X in F3() by A1;
hence x in F3() . i by A3, A6, PBOOLE:def 4; :: thesis: verum