assume A1:
for X being ManySortedSet of F_{1}() holds

( X in F_{2}() iff ( X in F_{3}() & P_{1}[X] ) )
; :: thesis: F_{2}() c= F_{3}()

consider K being ManySortedSet of F_{1}() such that

A2: K in F_{2}()
by PBOOLE:134;

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in F_{1}() or F_{2}() . i c= F_{3}() . i )

assume A3: i in F_{1}()
; :: thesis: F_{2}() . i c= F_{3}() . i

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F_{2}() . i or x in F_{3}() . i )

assume A4: x in F_{2}() . i
; :: thesis: x in F_{3}() . i

dom (K +* (i .--> x)) = F_{1}()
by A3, PZFMISC1:1;

then reconsider X = K +* (i .--> x) as ManySortedSet of F_{1}() by PARTFUN1:def 2, RELAT_1:def 18;

A5: dom (i .--> x) = {i} ;

i in {i} by TARSKI:def 1;

then A6: X . i = (i .--> x) . i by A5, FUNCT_4:13

.= x by FUNCOP_1:72 ;

X in F_{2}()
_{3}()
by A1;

hence x in F_{3}() . i
by A3, A6; :: thesis: verum

( X in F

consider K being ManySortedSet of F

A2: K in F

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in F

assume A3: i in F

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F

assume A4: x in F

dom (K +* (i .--> x)) = F

then reconsider X = K +* (i .--> x) as ManySortedSet of F

A5: dom (i .--> x) = {i} ;

i in {i} by TARSKI:def 1;

then A6: X . i = (i .--> x) . i by A5, FUNCT_4:13

.= x by FUNCOP_1:72 ;

X in F

proof

then
X in F
let s be object ; :: according to PBOOLE:def 1 :: thesis: ( not s in F_{1}() or X . s in F_{2}() . s )

assume A7: s in F_{1}()
; :: thesis: X . s in F_{2}() . s

end;assume A7: s in F

hence x in F