set P = { p where p is F1() -element XFinSequence of NAT : P1[p] } ;
set Q = { q where q is F1() -element XFinSequence of NAT : P2[q] } ;
thus { p where p is F1() -element XFinSequence of NAT : P1[p] } c= { q where q is F1() -element XFinSequence of NAT : P2[q] } :: according to XBOOLE_0:def 10 :: thesis: { q where q is F1() -element XFinSequence of NAT : P2[q] } c= { p where p is F1() -element XFinSequence of NAT : P1[p] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is F1() -element XFinSequence of NAT : P1[p] } or x in { q where q is F1() -element XFinSequence of NAT : P2[q] } )
assume A2: x in { p where p is F1() -element XFinSequence of NAT : P1[p] } ; :: thesis: x in { q where q is F1() -element XFinSequence of NAT : P2[q] }
consider p being F1() -element XFinSequence of NAT such that
A3: ( x = p & P1[p] ) by A2;
P2[p] by A1, A3;
hence x in { q where q is F1() -element XFinSequence of NAT : P2[q] } by A3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is F1() -element XFinSequence of NAT : P2[q] } or x in { p where p is F1() -element XFinSequence of NAT : P1[p] } )
assume A4: x in { q where q is F1() -element XFinSequence of NAT : P2[q] } ; :: thesis: x in { p where p is F1() -element XFinSequence of NAT : P1[p] }
consider p being F1() -element XFinSequence of NAT such that
A5: ( x = p & P2[p] ) by A4;
P1[p] by A1, A5;
hence x in { p where p is F1() -element XFinSequence of NAT : P1[p] } by A5; :: thesis: verum