set P = { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } ;

set Q = { q where q is F_{1}() -element XFinSequence of NAT : P_{2}[q] } ;

thus { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } c= { q where q is F_{1}() -element XFinSequence of NAT : P_{2}[q] }
:: according to XBOOLE_0:def 10 :: thesis: { q where q is F_{1}() -element XFinSequence of NAT : P_{2}[q] } c= { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } _{1}() -element XFinSequence of NAT : P_{2}[q] } or x in { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } )

assume A4: x in { q where q is F_{1}() -element XFinSequence of NAT : P_{2}[q] }
; :: thesis: x in { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] }

consider p being F_{1}() -element XFinSequence of NAT such that

A5: ( x = p & P_{2}[p] )
by A4;

P_{1}[p]
by A1, A5;

hence x in { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] }
by A5; :: thesis: verum

set Q = { q where q is F

thus { p where p is F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } or x in { q where q is F_{1}() -element XFinSequence of NAT : P_{2}[q] } )

assume A2: x in { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] }
; :: thesis: x in { q where q is F_{1}() -element XFinSequence of NAT : P_{2}[q] }

consider p being F_{1}() -element XFinSequence of NAT such that

A3: ( x = p & P_{1}[p] )
by A2;

P_{2}[p]
by A1, A3;

hence x in { q where q is F_{1}() -element XFinSequence of NAT : P_{2}[q] }
by A3; :: thesis: verum

end;assume A2: x in { p where p is F

consider p being F

A3: ( x = p & P

P

hence x in { q where q is F

assume A4: x in { q where q is F

consider p being F

A5: ( x = p & P

P

hence x in { p where p is F